| Author | Object | Transaction | Date |
|---|
| makarius | rISABELLE5469bacf5573: avoid duplicate Timing messages (see also 5c4800f6b25a); | | Aug 7 2020, 12:09 AM |
| makarius | rISABELLE5c4800f6b25a: more robust protocol for "Timing ..." messages, notably for pide_session=true; | | Aug 7 2020, 12:09 AM |
| makarius | rISABELLE411b3dc036ca: recovered stderr for PIDE batch-build, such as "Browser info at ...", "Document… | | Aug 7 2020, 12:09 AM |
| makarius | rISABELLEae683a461c40: merged | | Aug 6 2020, 11:46 PM |
| makarius | rISABELLE411b3dc036ca: recovered stderr for PIDE batch-build, such as "Browser info at ...", "Document… | | Aug 6 2020, 11:44 PM |
| makarius | rISABELLE1b06ed254943: more compact command_timings, as in former batch-build; | | Aug 6 2020, 11:27 PM |
| makarius | rISABELLE36743e0e2c4c: unused; | | Aug 6 2020, 11:13 PM |
| makarius | rISABELLEa1fb4d28e609: unused --- superseded by PIDE messages; | | Aug 6 2020, 10:58 PM |
| makarius | rISABELLEd9a42786fbc9: more thorough cleanup, e.g. before ML_Heap.save; | | Aug 6 2020, 10:54 PM |
| makarius | rISABELLE7b318273a4aa: discontinued old batch-build functionality; | | Aug 6 2020, 10:43 PM |
| dcjm | rPOLYMLde60abadc84f: Merge branch 'master' into ExecuteWrite | | Aug 6 2020, 6:24 PM |
| dcjm | rPOLYML59232968ed60: Posix.Process.exit should call PolyFinish rather than PolyTerminate so that… | | Aug 6 2020, 5:55 PM |
| nipkow | rISABELLEc65614b556b2: merged | | Aug 6 2020, 5:51 PM |
| nipkow | rISABELLE9fa6dde8d959: tuned | | Aug 6 2020, 5:39 PM |
| florian.haftmann | rISABELLE0b21b2beadb5: tailored towards remaining essence | | Aug 6 2020, 5:37 PM |
| florian.haftmann | rAFP116a82414c28: dropped alias | | Aug 6 2020, 5:32 PM |
| dcjm | rPOLYML88a6eca436ec: Use O_TMPFILE on Linux to create the temporary file for mapping. Saves having… | | Aug 6 2020, 5:17 PM |
| nipkow | rISABELLEf978ecaf119a: added theory Tree23_of_List | | Aug 6 2020, 5:11 PM |
| makarius | rISABELLE8c547eac8381: more robust treatment of thm_names, with strict check after all theories are… | | Aug 6 2020, 4:45 PM |
| paulson <lp15@cam.ac.uk> | rISABELLE496cfe488d72: a few more lemmas | | Aug 6 2020, 2:07 PM |
| dcjm | rPOLYMLe51f00cccb0a: Tidy-up shutdown of statistics. | | Aug 6 2020, 1:38 PM |
| dcjm | rPOLYMLcbd49e8ae6cd: Fix changes to statistics.cpp for Windows. | | Aug 6 2020, 1:24 PM |
| dcjm | rPOLYMLc1ff455836c7: Unlink any existing statistics file. Open will fail if it exists. Report an… | | Aug 6 2020, 1:15 PM |
| dcjm | rPOLYML8e4d341bd778: Check inside the simplifier that the body of a potential inline function is… | | Aug 6 2020, 8:40 AM |
| dcjm | rPOLYML4c21a9d8e5e7: Small change to 8e4d341 to allow compilation when int is IntInf.int. | | Aug 6 2020, 8:40 AM |
| dcjm | rPOLYML4c21a9d8e5e7: Small change to 8e4d341 to allow compilation when int is IntInf.int. | | Aug 6 2020, 8:14 AM |
| paulson | rISABELLE6b5421bd0fc3: merged | | Aug 5 2020, 10:03 PM |
| paulson <lp15@cam.ac.uk> | rISABELLEcfb6c22a5636: lemmas about sets and the enumerate operator | | Aug 5 2020, 8:12 PM |
| florian.haftmann | rISABELLEa36db1c8238e: separation of reversed bit lists from other material | | Aug 5 2020, 7:06 PM |
| paulson <lp15@cam.ac.uk> | rISABELLEbeccb2a0410f: yet another little lemma | | Aug 5 2020, 6:56 PM |
| paulson | rISABELLE6a2f43901350: merged | | Aug 5 2020, 6:50 PM |
| florian.haftmann | rAFP3e79743d7844: separation of reversed bit lists from other material | | Aug 5 2020, 6:33 PM |
| makarius | rISABELLE43a43b182a81: merged | | Aug 5 2020, 5:19 PM |
| makarius | rISABELLE41e1e2395a67: avoid exhaustion of worker threads, notably due to complex interaction of… | | Aug 5 2020, 4:16 PM |
| makarius | rISABELLE3afd6b1c7ab5: more robust: insist in finished future; | | Aug 5 2020, 12:42 PM |
| makarius | rISABELLEdf99d26efeeb: unused; | | Aug 5 2020, 12:34 PM |
| florian.haftmann | rAFPcac1c67360f3: further refinement of code equations for mask operation | | Aug 5 2020, 10:47 AM |
| florian.haftmann | rISABELLE3ec876181527: further refinement of code equations for mask operation | | Aug 5 2020, 10:47 AM |
| dcjm | rPOLYML9fd706535dad: Add MAP_STACK in 32-in-64 for OpenBSD. | | Aug 4 2020, 6:54 PM |
| dcjm | rPOLYML9691933b9055: Support 32-in-64 on OSs that disallow write+execute. | | Aug 4 2020, 6:38 PM |
| dcjm | rPOLYML985effca050e: Fix changes for Unix. | | Aug 4 2020, 5:45 PM |
| dcjm | rPOLYML0283ba475549: Split the Windows and Unix versions of the allocators. | | Aug 4 2020, 5:29 PM |
| paulson <lp15@cam.ac.uk> | rAFP0f761b3bffa8: sitegen for Chandy_Lamport | | Aug 4 2020, 1:34 PM |
| paulson <lp15@cam.ac.uk> | rAFPdf750599e814: new entry Chandy_Lamport | | Aug 4 2020, 1:25 PM |
| paulson | rISABELLE3f8e6c0166ac: merged | | Aug 4 2020, 12:45 PM |
| florian.haftmann | rISABELLE41393ecb57ac: uniform mask operation | | Aug 4 2020, 11:33 AM |
| florian.haftmann | rAFPf28d68deefa8: uniform mask operation | | Aug 4 2020, 11:24 AM |
| florian.haftmann | rAFP52ddcd32c0c9: clearer separation of pre-word bit list material | | Aug 4 2020, 11:24 AM |
| florian.haftmann | rISABELLEe4d42f5766dc: clearer separation of pre-word bit list material | | Aug 4 2020, 11:24 AM |
| florian.haftmann | rAFP9b629e0e6654: repaired document slip | | Aug 4 2020, 7:18 AM |
| dcjm | rPOLYML1507c82e4597: Merge branch 'ExecuteWrite' of https://github.com/dcjm/polyml into ExecuteWrite | | Aug 3 2020, 11:24 PM |
| dcjm | rPOLYMLd91625d272a2: Add an extra section when exporting on Linux to mark the stack as non… | | Aug 3 2020, 11:24 PM |
| dcjm | rPOLYML8a09919cf1cd: Should be @progbits not %. | | Aug 3 2020, 11:04 PM |
| dcjm | rPOLYML8fc5b4b3ebb6: Remove the configure test for the non-executable stack flag and instead use it… | | Aug 3 2020, 9:15 PM |
| dcjm | rPOLYML367fef5e6815: Merge branch 'ExecuteWrite' of https://github.com/dcjm/polyml into ExecuteWrite | | Aug 3 2020, 8:34 PM |
| dcjm | rPOLYML3d76a242f156: Mmap with execute+write returns EACCES in SElinux. | | Aug 3 2020, 8:34 PM |
| dcjm | rPOLYML9f0a6109d720: Fixes to compile on Linux. | | Aug 3 2020, 4:35 PM |
| dcjm | rPOLYML0fc89def32f3: Change from boolean executable/non-executable into a three-way selection… | | Aug 3 2020, 4:31 PM |
| nipkow | rISABELLE2030eacf3a72: added lemma | | Aug 3 2020, 4:21 PM |
| dcjm | rPOLYML1b579fda5f12: Implement dual areas if mmap fails when write+execute permission is requested. | | Aug 3 2020, 2:26 PM |
| paulson | rISABELLEb6065cbbf5e2: merged | | Aug 3 2020, 12:46 PM |
| florian.haftmann | rAFPef3c8932106a: more consequent transferability | | Aug 1 2020, 7:43 PM |
| florian.haftmann | rISABELLE8c355e2dd7db: more consequent transferability | | Aug 1 2020, 7:43 PM |
| dcjm | rPOLYML89f0cb1022d7: When trying to write to the code area write to the shadow area instead. This… | | Aug 1 2020, 6:19 PM |
| paulson <lp15@cam.ac.uk> | rISABELLE5d17e7a0825a: strengthened a lemma | | Jul 31 2020, 9:38 PM |
| dcjm | rPOLYML81ea85843cc2: The interpreted version does not need "code" to have execute permission because… | | Jul 31 2020, 5:41 PM |
| dcjm | rPOLYML48cb2b24ff27: Revert "Remove FlushInstructionCache" d3c42ae. We may need this for the ARM… | | Jul 31 2020, 5:09 PM |
| paulson <lp15@cam.ac.uk> | rISABELLE8348bba699e6: A new lemma about abstract Sum / Prod | | Jul 31 2020, 1:54 PM |
| dcjm | rPOLYML49c0cc4cbaed: Change osmem.cpp for Linux. | | Jul 30 2020, 7:39 PM |
| dcjm | rPOLYMLd82478675931: Change the low-level allocator to separate out code and data allocation. | | Jul 30 2020, 7:17 PM |
| dcjm | rPOLYMLd471c5e6e1cf: Update compiler version to 5.8.2 so that we pick up the correct files on… | | Jul 30 2020, 1:42 PM |
| dcjm | rPOLYML8e4d341bd778: Check inside the simplifier that the body of a potential inline function is… | | Jul 30 2020, 1:40 PM |
| dcjm | rPOLYML6442ac3a51c6: Remove unused parameters. | | Jul 30 2020, 11:55 AM |
| dcjm | rPOLYML654e1adee079: Merge branch 'master' of github.com:dcjm/polyml | | Jul 29 2020, 6:24 PM |
| dcjm | rPOLYML5dc69bc3a7d5: Search for machine/reloc.h separately from elf_abi.h. These seem to have been… | | Jul 29 2020, 6:23 PM |
| dcjm | rPOLYML7d72f11eeab9: Change all the casts from PolyWord* to stackItem*. Some had been missed. | | Jul 29 2020, 6:18 PM |
| makarius | rISABELLEb8d0b8659e0a: more robust scheduler shutdown, notably for spurious crashes; | | Jul 29 2020, 2:23 PM |
| nipkow | rAFP0252745a70fc: new entry Relational_Paths | | Jul 28 2020, 9:50 AM |
| nipkow | rISABELLE1d6c3cba47fe: unclear why I ever asked for type tree2 | | Jul 27 2020, 3:58 PM |
| makarius | rISABELLEbd9d1ce274c9: enforce pide_session to see if all isabelle_cronjob tasks work smoothly with it; | | Jul 26 2020, 10:28 PM |
| makarius | rISABELLE9c0b835d4cc2: proper pretty printing for latex output, notably for pide_session=true… | | Jul 26 2020, 9:53 PM |
| makarius | rISABELLEf3e1144a1cec: clarified name to avoid duplication (no distinction of data on host =… | | Jul 25 2020, 11:23 PM |
| makarius | rISABELLEf56522a44564: clarified names; | | Jul 25 2020, 9:09 PM |
| makarius | rISABELLEfed7b0ae20d8: more errors; | | Jul 25 2020, 12:43 PM |
| makarius | rISABELLEbad75618fb82: extraction of equations x = t from premises beneath meta-all | | Jul 24 2020, 10:38 PM |
| makarius | rAFP40e16c534243: much faster proofs (cf. Isabelle/bad75618fb82); | | Jul 24 2020, 10:38 PM |
| makarius | rAFP40e16c534243: much faster proofs (cf. Isabelle/bad75618fb82); | | Jul 24 2020, 10:09 PM |
| makarius | rISABELLEd3cad9ecd0cc: follow Phabricator update 2020 Week 27; | | Jul 24 2020, 8:43 PM |
| Achim D. Brucker <adbrucker@0x5f.org> | rAFP7757456aafcf: Fixed failing proofs. | | Jul 24 2020, 8:17 PM |
| makarius | rISABELLEb17be02a0a11: tuned; | | Jul 24 2020, 4:45 PM |
| makarius | rISABELLE9cde8c4ea5a5: discontinued obsolete "isabelle imports" and all_known data; | | Jul 24 2020, 3:37 PM |
| makarius | rISABELLEce844442e2ab: obsolete (see 9cde8c4ea5a5); | | Jul 24 2020, 3:37 PM |
| makarius | rISABELLEebf3ba74bc4c: unused; | | Jul 24 2020, 3:20 PM |
| makarius | rISABELLE4768b1facec2: clarified errors: avoid hiding of import_errors/dir_errors by their… | | Jul 24 2020, 3:02 PM |
| dcjm | rPOLYMLc89f66c8ee6e: The abi type is always a short int. | | Jul 24 2020, 1:54 PM |
| dcjm | rPOLYMLbbfff949ac36: Merge branch 'master' into CompileForeignCall | | Jul 24 2020, 1:36 PM |
| dcjm | rPOLYML196ac3bc7d11: Move the test for the result of PolyCompareArbitrary up to the top-level of… | | Jul 24 2020, 1:08 PM |
| dcjm | rPOLYMLb9e4e5128d56: Merge commit '196ac3bc7d11b43f488fb945077aac162144bd31' | | Jul 24 2020, 1:08 PM |
| Achim D. Brucker <adbrucker@0x5f.org> | rAFP34a339f71b38: Added proofs about get_tag_type. | | Jul 24 2020, 12:54 PM |
| dcjm | rPOLYML7e214665fa88: Remove push and pop of rcx/ecx in CALL_EXTRA macro. This seems to be a relic… | | Jul 24 2020, 12:39 PM |