| Author | Object | Transaction | Date |
|---|
| makarius | rISABELLE2831933195ef: NEWS; | | Fri, Aug 7, 11:33 PM |
| makarius | Blog Post: ML statistics via an external Poly/ML process | makarius set this post's subtitle to "". | Fri, Aug 7, 11:33 PM |
| makarius | Blog Post: ML statistics via an external Poly/ML process | | Fri, Aug 7, 11:33 PM |
| makarius | Blog Post: ML statistics via an external Poly/ML process | | Fri, Aug 7, 11:33 PM |
| makarius | Blog Post: ML statistics via an external Poly/ML process | makarius renamed this blog post from to ML statistics via an external Poly/ML process. | Fri, Aug 7, 11:33 PM |
| makarius | Blog Post: ML statistics via an external Poly/ML process | | Fri, Aug 7, 11:33 PM |
| makarius | Blog Post: ML statistics via an external Poly/ML process | | Fri, Aug 7, 11:33 PM |
| makarius | rPOLYML52881757b127: The shared memory file for remote statistics on Unix is now in $POLYSTATSDIR if… | | Fri, Aug 7, 11:32 PM |
| makarius | rISABELLEd115d50a19c0: provide POLYSTATSDIR to keep $HOME/.polyml clean (requires Poly/ML 52881757b127… | | Fri, Aug 7, 11:32 PM |
| makarius | rISABELLE7b318273a4aa: discontinued old batch-build functionality; | | Fri, Aug 7, 11:32 PM |
| makarius | rISABELLE84f716e72fa3: adapted to 7b318273a4aa; | | Fri, Aug 7, 11:32 PM |
| makarius | rISABELLE2831933195ef: NEWS; | | Fri, Aug 7, 11:01 PM |
| makarius | rISABELLEd115d50a19c0: provide POLYSTATSDIR to keep $HOME/.polyml clean (requires Poly/ML 52881757b127… | | Fri, Aug 7, 10:57 PM |
| makarius | rISABELLE84f716e72fa3: adapted to 7b318273a4aa; | | Fri, Aug 7, 10:28 PM |
| makarius | rISABELLE4d8b3209dae3: cache props; | | Fri, Aug 7, 10:23 PM |
| makarius | rISABELLE7773ec172572: clarified names; | | Fri, Aug 7, 10:19 PM |
| makarius | rISABELLEc998827f1df9: more thorough protocol_handlers.exit, like file_formats.stop_session; | | Fri, Aug 7, 9:21 PM |
| makarius | rISABELLEd00220799735: tuned names; | | Fri, Aug 7, 9:02 PM |
| makarius | rISABELLE2d9e40cfe9af: temporary workaround for 100% CPU usage in OS.Process.sleep; | | Fri, Aug 7, 8:28 PM |
| makarius | rISABELLE3546dd4ade74: ML statistics via external process: allows monitoring RTS while ML program… | | Fri, Aug 7, 8:19 PM |
| dcjm | rPOLYMLf80d20c14967: Some clean up of remote statistics in Windows. | | Fri, Aug 7, 5:39 PM |
| dcjm | rPOLYML52881757b127: The shared memory file for remote statistics on Unix is now in $POLYSTATSDIR if… | | Fri, Aug 7, 4:12 PM |
| makarius | rISABELLEb9ded33bd58c: clarified catch-all handler --- avoid confusion of Interrupt vs. Exn.Interrupt… | | Fri, Aug 7, 3:13 PM |
| makarius | rISABELLE16fab31feadc: avoid failure of "isabelle build -o skip_proofs"; | | Fri, Aug 7, 11:46 AM |
| makarius | rISABELLE940195fbb282: clarified messages; | | Fri, Aug 7, 12:09 AM |
| makarius | rISABELLE5469bacf5573: avoid duplicate Timing messages (see also 5c4800f6b25a); | | Fri, Aug 7, 12:09 AM |
| makarius | rISABELLE5c4800f6b25a: more robust protocol for "Timing ..." messages, notably for pide_session=true; | | Fri, Aug 7, 12:09 AM |
| makarius | rISABELLE411b3dc036ca: recovered stderr for PIDE batch-build, such as "Browser info at ...", "Document… | | Fri, Aug 7, 12:09 AM |
| makarius | rISABELLEae683a461c40: merged | | Thu, Aug 6, 11:46 PM |
| makarius | rISABELLE411b3dc036ca: recovered stderr for PIDE batch-build, such as "Browser info at ...", "Document… | | Thu, Aug 6, 11:44 PM |
| makarius | rISABELLE1b06ed254943: more compact command_timings, as in former batch-build; | | Thu, Aug 6, 11:27 PM |
| makarius | rISABELLE36743e0e2c4c: unused; | | Thu, Aug 6, 11:13 PM |
| makarius | rISABELLEa1fb4d28e609: unused --- superseded by PIDE messages; | | Thu, Aug 6, 10:58 PM |
| makarius | rISABELLEd9a42786fbc9: more thorough cleanup, e.g. before ML_Heap.save; | | Thu, Aug 6, 10:54 PM |
| makarius | rISABELLE7b318273a4aa: discontinued old batch-build functionality; | | Thu, Aug 6, 10:43 PM |
| dcjm | rPOLYML59232968ed60: Posix.Process.exit should call PolyFinish rather than PolyTerminate so that… | | Thu, Aug 6, 5:55 PM |
| nipkow | rISABELLEc65614b556b2: merged | | Thu, Aug 6, 5:51 PM |
| nipkow | rISABELLE9fa6dde8d959: tuned | | Thu, Aug 6, 5:39 PM |
| florian.haftmann | rISABELLE0b21b2beadb5: tailored towards remaining essence | | Thu, Aug 6, 5:37 PM |
| florian.haftmann | rAFP116a82414c28: dropped alias | | Thu, Aug 6, 5:32 PM |
| nipkow | rISABELLEf978ecaf119a: added theory Tree23_of_List | | Thu, Aug 6, 5:11 PM |
| makarius | rISABELLE8c547eac8381: more robust treatment of thm_names, with strict check after all theories are… | | Thu, Aug 6, 4:45 PM |
| paulson <lp15@cam.ac.uk> | rISABELLE496cfe488d72: a few more lemmas | | Thu, Aug 6, 2:07 PM |
| dcjm | rPOLYMLe51f00cccb0a: Tidy-up shutdown of statistics. | | Thu, Aug 6, 1:38 PM |
| dcjm | rPOLYMLcbd49e8ae6cd: Fix changes to statistics.cpp for Windows. | | Thu, Aug 6, 1:24 PM |
| dcjm | rPOLYMLc1ff455836c7: Unlink any existing statistics file. Open will fail if it exists. Report an… | | Thu, Aug 6, 1:15 PM |
| dcjm | rPOLYML8e4d341bd778: Check inside the simplifier that the body of a potential inline function is… | | Thu, Aug 6, 8:40 AM |
| dcjm | rPOLYML4c21a9d8e5e7: Small change to 8e4d341 to allow compilation when int is IntInf.int. | | Thu, Aug 6, 8:40 AM |
| dcjm | rPOLYML4c21a9d8e5e7: Small change to 8e4d341 to allow compilation when int is IntInf.int. | | Thu, Aug 6, 8:14 AM |
| paulson | rISABELLE6b5421bd0fc3: merged | | Wed, Aug 5, 10:03 PM |
| paulson <lp15@cam.ac.uk> | rISABELLEcfb6c22a5636: lemmas about sets and the enumerate operator | | Wed, Aug 5, 8:12 PM |
| florian.haftmann | rISABELLEa36db1c8238e: separation of reversed bit lists from other material | | Wed, Aug 5, 7:06 PM |
| paulson <lp15@cam.ac.uk> | rISABELLEbeccb2a0410f: yet another little lemma | | Wed, Aug 5, 6:56 PM |
| paulson | rISABELLE6a2f43901350: merged | | Wed, Aug 5, 6:50 PM |
| florian.haftmann | rAFP3e79743d7844: separation of reversed bit lists from other material | | Wed, Aug 5, 6:33 PM |
| makarius | rISABELLE43a43b182a81: merged | | Wed, Aug 5, 5:19 PM |
| makarius | rISABELLE41e1e2395a67: avoid exhaustion of worker threads, notably due to complex interaction of… | | Wed, Aug 5, 4:16 PM |
| makarius | rISABELLE3afd6b1c7ab5: more robust: insist in finished future; | | Wed, Aug 5, 12:42 PM |
| makarius | rISABELLEdf99d26efeeb: unused; | | Wed, Aug 5, 12:34 PM |
| florian.haftmann | rAFPcac1c67360f3: further refinement of code equations for mask operation | | Wed, Aug 5, 10:47 AM |
| florian.haftmann | rISABELLE3ec876181527: further refinement of code equations for mask operation | | Wed, Aug 5, 10:47 AM |
| paulson | rISABELLE3f8e6c0166ac: merged | | Tue, Aug 4, 12:45 PM |
| florian.haftmann | rISABELLE41393ecb57ac: uniform mask operation | | Tue, Aug 4, 11:33 AM |
| florian.haftmann | rAFPf28d68deefa8: uniform mask operation | | Tue, Aug 4, 11:24 AM |
| florian.haftmann | rAFP52ddcd32c0c9: clearer separation of pre-word bit list material | | Tue, Aug 4, 11:24 AM |
| florian.haftmann | rISABELLEe4d42f5766dc: clearer separation of pre-word bit list material | | Tue, Aug 4, 11:24 AM |
| florian.haftmann | rAFP9b629e0e6654: repaired document slip | | Tue, Aug 4, 7:18 AM |
| nipkow | rISABELLE2030eacf3a72: added lemma | | Mon, Aug 3, 4:21 PM |
| paulson | rISABELLEb6065cbbf5e2: merged | | Mon, Aug 3, 12:46 PM |
| florian.haftmann | rAFPef3c8932106a: more consequent transferability | | Sat, Aug 1, 7:43 PM |
| florian.haftmann | rISABELLE8c355e2dd7db: more consequent transferability | | Sat, Aug 1, 7:43 PM |
| paulson <lp15@cam.ac.uk> | rISABELLE5d17e7a0825a: strengthened a lemma | | Fri, Jul 31, 9:38 PM |
| paulson <lp15@cam.ac.uk> | rISABELLE8348bba699e6: A new lemma about abstract Sum / Prod | | Fri, Jul 31, 1:54 PM |
| dcjm | rPOLYMLd471c5e6e1cf: Update compiler version to 5.8.2 so that we pick up the correct files on… | | Thu, Jul 30, 1:42 PM |
| dcjm | rPOLYML8e4d341bd778: Check inside the simplifier that the body of a potential inline function is… | | Thu, Jul 30, 1:40 PM |
| dcjm | rPOLYML6442ac3a51c6: Remove unused parameters. | | Thu, Jul 30, 11:55 AM |
| dcjm | rPOLYML654e1adee079: Merge branch 'master' of github.com:dcjm/polyml | | Wed, Jul 29, 6:24 PM |
| dcjm | rPOLYML5dc69bc3a7d5: Search for machine/reloc.h separately from elf_abi.h. These seem to have been… | | Wed, Jul 29, 6:23 PM |
| dcjm | rPOLYML7d72f11eeab9: Change all the casts from PolyWord* to stackItem*. Some had been missed. | | Wed, Jul 29, 6:18 PM |
| makarius | rISABELLEb8d0b8659e0a: more robust scheduler shutdown, notably for spurious crashes; | | Wed, Jul 29, 2:23 PM |
| nipkow | rISABELLE1d6c3cba47fe: unclear why I ever asked for type tree2 | | Mon, Jul 27, 3:58 PM |
| makarius | rISABELLEbd9d1ce274c9: enforce pide_session to see if all isabelle_cronjob tasks work smoothly with it; | | Sun, Jul 26, 10:28 PM |
| makarius | rISABELLE9c0b835d4cc2: proper pretty printing for latex output, notably for pide_session=true… | | Sun, Jul 26, 9:53 PM |
| makarius | rISABELLEf3e1144a1cec: clarified name to avoid duplication (no distinction of data on host =… | | Sat, Jul 25, 11:23 PM |
| makarius | rISABELLEf56522a44564: clarified names; | | Sat, Jul 25, 9:09 PM |
| makarius | rISABELLEfed7b0ae20d8: more errors; | | Sat, Jul 25, 12:43 PM |
| makarius | rISABELLEbad75618fb82: extraction of equations x = t from premises beneath meta-all | | Fri, Jul 24, 10:38 PM |
| makarius | rAFP40e16c534243: much faster proofs (cf. Isabelle/bad75618fb82); | | Fri, Jul 24, 10:38 PM |
| makarius | rAFP40e16c534243: much faster proofs (cf. Isabelle/bad75618fb82); | | Fri, Jul 24, 10:09 PM |
| makarius | rISABELLEd3cad9ecd0cc: follow Phabricator update 2020 Week 27; | | Fri, Jul 24, 8:43 PM |
| Achim D. Brucker <adbrucker@0x5f.org> | rAFP7757456aafcf: Fixed failing proofs. | | Fri, Jul 24, 8:17 PM |
| makarius | rISABELLEb17be02a0a11: tuned; | | Fri, Jul 24, 4:45 PM |
| makarius | rISABELLE9cde8c4ea5a5: discontinued obsolete "isabelle imports" and all_known data; | | Fri, Jul 24, 3:37 PM |
| makarius | rISABELLEce844442e2ab: obsolete (see 9cde8c4ea5a5); | | Fri, Jul 24, 3:37 PM |
| makarius | rISABELLEebf3ba74bc4c: unused; | | Fri, Jul 24, 3:20 PM |
| makarius | rISABELLE4768b1facec2: clarified errors: avoid hiding of import_errors/dir_errors by their… | | Fri, Jul 24, 3:02 PM |
| dcjm | rPOLYML196ac3bc7d11: Move the test for the result of PolyCompareArbitrary up to the top-level of… | | Fri, Jul 24, 1:08 PM |
| dcjm | rPOLYMLb9e4e5128d56: Merge commit '196ac3bc7d11b43f488fb945077aac162144bd31' | | Fri, Jul 24, 1:08 PM |
| Achim D. Brucker <adbrucker@0x5f.org> | rAFP34a339f71b38: Added proofs about get_tag_type. | | Fri, Jul 24, 12:54 PM |
| dcjm | rPOLYML7e214665fa88: Remove push and pop of rcx/ecx in CALL_EXTRA macro. This seems to be a relic… | | Fri, Jul 24, 12:39 PM |