Page MenuHomeIsabelle/Phabricator
Feed All Transactions
AuthorObjectTransactionDate
makariusrISABELLE2831933195ef: NEWS;Fri, Aug 7, 11:33 PM
makariusBlog Post: ML statistics via an external Poly/ML process
makarius set this post's subtitle to "". 
Fri, Aug 7, 11:33 PM
makariusBlog Post: ML statistics via an external Poly/ML process
makarius updated the post content. 
Fri, Aug 7, 11:33 PM
makariusBlog Post: ML statistics via an external Poly/ML process
makarius published this post. 
Fri, Aug 7, 11:33 PM
makariusBlog 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
makariusBlog Post: ML statistics via an external Poly/ML processFri, Aug 7, 11:33 PM
makariusBlog Post: ML statistics via an external Poly/ML process
makarius created this post. 
Fri, Aug 7, 11:33 PM
makariusrPOLYML52881757b127: The shared memory file for remote statistics on Unix is now in $POLYSTATSDIR if…Fri, Aug 7, 11:32 PM
makariusrISABELLEd115d50a19c0: provide POLYSTATSDIR to keep $HOME/.polyml clean (requires Poly/ML 52881757b127…Fri, Aug 7, 11:32 PM
makariusrISABELLE7b318273a4aa: discontinued old batch-build functionality;Fri, Aug 7, 11:32 PM
makariusrISABELLE84f716e72fa3: adapted to 7b318273a4aa;Fri, Aug 7, 11:32 PM
makariusrISABELLE2831933195ef: NEWS;Fri, Aug 7, 11:01 PM
makariusrISABELLEd115d50a19c0: provide POLYSTATSDIR to keep $HOME/.polyml clean (requires Poly/ML 52881757b127…Fri, Aug 7, 10:57 PM
makariusrISABELLE84f716e72fa3: adapted to 7b318273a4aa;Fri, Aug 7, 10:28 PM
makariusrISABELLE4d8b3209dae3: cache props;Fri, Aug 7, 10:23 PM
makariusrISABELLE7773ec172572: clarified names;Fri, Aug 7, 10:19 PM
makariusrISABELLEc998827f1df9: more thorough protocol_handlers.exit, like file_formats.stop_session;Fri, Aug 7, 9:21 PM
makariusrISABELLEd00220799735: tuned names;Fri, Aug 7, 9:02 PM
makariusrISABELLE2d9e40cfe9af: temporary workaround for 100% CPU usage in OS.Process.sleep;Fri, Aug 7, 8:28 PM
makariusrISABELLE3546dd4ade74: ML statistics via external process: allows monitoring RTS while ML program…Fri, Aug 7, 8:19 PM
dcjmrPOLYMLf80d20c14967: Some clean up of remote statistics in Windows.Fri, Aug 7, 5:39 PM
dcjmrPOLYML52881757b127: The shared memory file for remote statistics on Unix is now in $POLYSTATSDIR if…Fri, Aug 7, 4:12 PM
makariusrISABELLEb9ded33bd58c: clarified catch-all handler --- avoid confusion of Interrupt vs. Exn.Interrupt…Fri, Aug 7, 3:13 PM
makariusrISABELLE16fab31feadc: avoid failure of "isabelle build -o skip_proofs";Fri, Aug 7, 11:46 AM
makariusrISABELLE940195fbb282: clarified messages;Fri, Aug 7, 12:09 AM
makariusrISABELLE5469bacf5573: avoid duplicate Timing messages (see also 5c4800f6b25a);Fri, Aug 7, 12:09 AM
makariusrISABELLE5c4800f6b25a: more robust protocol for "Timing ..." messages, notably for pide_session=true;Fri, Aug 7, 12:09 AM
makariusrISABELLE411b3dc036ca: recovered stderr for PIDE batch-build, such as "Browser info at ...", "Document…Fri, Aug 7, 12:09 AM
makariusrISABELLEae683a461c40: mergedThu, Aug 6, 11:46 PM
makariusrISABELLE411b3dc036ca: recovered stderr for PIDE batch-build, such as "Browser info at ...", "Document…Thu, Aug 6, 11:44 PM
makariusrISABELLE1b06ed254943: more compact command_timings, as in former batch-build;Thu, Aug 6, 11:27 PM
makariusrISABELLE36743e0e2c4c: unused;Thu, Aug 6, 11:13 PM
makariusrISABELLEa1fb4d28e609: unused --- superseded by PIDE messages;Thu, Aug 6, 10:58 PM
makariusrISABELLEd9a42786fbc9: more thorough cleanup, e.g. before ML_Heap.save;Thu, Aug 6, 10:54 PM
makariusrISABELLE7b318273a4aa: discontinued old batch-build functionality;Thu, Aug 6, 10:43 PM
dcjmrPOLYML59232968ed60: Posix.Process.exit should call PolyFinish rather than PolyTerminate so that…Thu, Aug 6, 5:55 PM
nipkowrISABELLEc65614b556b2: merged
nipkow committed rISABELLEc65614b556b2: merged. 
Thu, Aug 6, 5:51 PM
nipkowrISABELLE9fa6dde8d959: tuned
nipkow committed rISABELLE9fa6dde8d959: tuned. 
Thu, Aug 6, 5:39 PM
florian.haftmannrISABELLE0b21b2beadb5: tailored towards remaining essenceThu, Aug 6, 5:37 PM
florian.haftmannrAFP116a82414c28: dropped aliasThu, Aug 6, 5:32 PM
nipkowrISABELLEf978ecaf119a: added theory Tree23_of_ListThu, Aug 6, 5:11 PM
makariusrISABELLE8c547eac8381: 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
paulson <lp15@cam.ac.uk> committed rISABELLE496cfe488d72: a few more lemmas. 
Thu, Aug 6, 2:07 PM
dcjmrPOLYMLe51f00cccb0a: Tidy-up shutdown of statistics.Thu, Aug 6, 1:38 PM
dcjmrPOLYMLcbd49e8ae6cd: Fix changes to statistics.cpp for Windows.Thu, Aug 6, 1:24 PM
dcjmrPOLYMLc1ff455836c7: Unlink any existing statistics file. Open will fail if it exists. Report an…Thu, Aug 6, 1:15 PM
dcjmrPOLYML8e4d341bd778: Check inside the simplifier that the body of a potential inline function is…Thu, Aug 6, 8:40 AM
dcjmrPOLYML4c21a9d8e5e7: Small change to 8e4d341 to allow compilation when int is IntInf.int.Thu, Aug 6, 8:40 AM
dcjmrPOLYML4c21a9d8e5e7: Small change to 8e4d341 to allow compilation when int is IntInf.int.Thu, Aug 6, 8:14 AM
paulsonrISABELLE6b5421bd0fc3: merged
paulson committed rISABELLE6b5421bd0fc3: merged. 
Wed, Aug 5, 10:03 PM
paulson <lp15@cam.ac.uk>rISABELLEcfb6c22a5636: lemmas about sets and the enumerate operatorWed, Aug 5, 8:12 PM
florian.haftmannrISABELLEa36db1c8238e: separation of reversed bit lists from other materialWed, Aug 5, 7:06 PM
paulson <lp15@cam.ac.uk>rISABELLEbeccb2a0410f: yet another little lemma
paulson <lp15@cam.ac.uk> committed rISABELLEbeccb2a0410f: yet another little lemma. 
Wed, Aug 5, 6:56 PM
paulsonrISABELLE6a2f43901350: merged
paulson committed rISABELLE6a2f43901350: merged. 
Wed, Aug 5, 6:50 PM
florian.haftmannrAFP3e79743d7844: separation of reversed bit lists from other materialWed, Aug 5, 6:33 PM
makariusrISABELLE43a43b182a81: mergedWed, Aug 5, 5:19 PM
makariusrISABELLE41e1e2395a67: avoid exhaustion of worker threads, notably due to complex interaction of…Wed, Aug 5, 4:16 PM
makariusrISABELLE3afd6b1c7ab5: more robust: insist in finished future;Wed, Aug 5, 12:42 PM
makariusrISABELLEdf99d26efeeb: unused;Wed, Aug 5, 12:34 PM
florian.haftmannrAFPcac1c67360f3: further refinement of code equations for mask operationWed, Aug 5, 10:47 AM
florian.haftmannrISABELLE3ec876181527: further refinement of code equations for mask operationWed, Aug 5, 10:47 AM
paulsonrISABELLE3f8e6c0166ac: merged
paulson committed rISABELLE3f8e6c0166ac: merged. 
Tue, Aug 4, 12:45 PM
florian.haftmannrISABELLE41393ecb57ac: uniform mask operationTue, Aug 4, 11:33 AM
florian.haftmannrAFPf28d68deefa8: uniform mask operationTue, Aug 4, 11:24 AM
florian.haftmannrAFP52ddcd32c0c9: clearer separation of pre-word bit list materialTue, Aug 4, 11:24 AM
florian.haftmannrISABELLEe4d42f5766dc: clearer separation of pre-word bit list materialTue, Aug 4, 11:24 AM
florian.haftmannrAFP9b629e0e6654: repaired document slipTue, Aug 4, 7:18 AM
nipkowrISABELLE2030eacf3a72: added lemmaMon, Aug 3, 4:21 PM
paulsonrISABELLEb6065cbbf5e2: merged
paulson committed rISABELLEb6065cbbf5e2: merged. 
Mon, Aug 3, 12:46 PM
florian.haftmannrAFPef3c8932106a: more consequent transferabilitySat, Aug 1, 7:43 PM
florian.haftmannrISABELLE8c355e2dd7db: more consequent transferabilitySat, Aug 1, 7:43 PM
paulson <lp15@cam.ac.uk>rISABELLE5d17e7a0825a: strengthened a lemma
paulson <lp15@cam.ac.uk> committed rISABELLE5d17e7a0825a: strengthened a lemma. 
Fri, Jul 31, 9:38 PM
paulson <lp15@cam.ac.uk>rISABELLE8348bba699e6: A new lemma about abstract Sum / ProdFri, Jul 31, 1:54 PM
dcjmrPOLYMLd471c5e6e1cf: Update compiler version to 5.8.2 so that we pick up the correct files on…Thu, Jul 30, 1:42 PM
dcjmrPOLYML8e4d341bd778: Check inside the simplifier that the body of a potential inline function is…Thu, Jul 30, 1:40 PM
dcjmrPOLYML6442ac3a51c6: Remove unused parameters.Thu, Jul 30, 11:55 AM
dcjmrPOLYML654e1adee079: Merge branch 'master' of github.com:dcjm/polymlWed, Jul 29, 6:24 PM
dcjmrPOLYML5dc69bc3a7d5: Search for machine/reloc.h separately from elf_abi.h. These seem to have been…Wed, Jul 29, 6:23 PM
dcjmrPOLYML7d72f11eeab9: Change all the casts from PolyWord* to stackItem*. Some had been missed.Wed, Jul 29, 6:18 PM
makariusrISABELLEb8d0b8659e0a: more robust scheduler shutdown, notably for spurious crashes;Wed, Jul 29, 2:23 PM
nipkowrISABELLE1d6c3cba47fe: unclear why I ever asked for type tree2Mon, Jul 27, 3:58 PM
makariusrISABELLEbd9d1ce274c9: enforce pide_session to see if all isabelle_cronjob tasks work smoothly with it;Sun, Jul 26, 10:28 PM
makariusrISABELLE9c0b835d4cc2: proper pretty printing for latex output, notably for pide_session=true…Sun, Jul 26, 9:53 PM
makariusrISABELLEf3e1144a1cec: clarified name to avoid duplication (no distinction of data on host =…Sat, Jul 25, 11:23 PM
makariusrISABELLEf56522a44564: clarified names;Sat, Jul 25, 9:09 PM
makariusrISABELLEfed7b0ae20d8: more errors;Sat, Jul 25, 12:43 PM
makariusrISABELLEbad75618fb82: extraction of equations x = t from premises beneath meta-allFri, Jul 24, 10:38 PM
makariusrAFP40e16c534243: much faster proofs (cf. Isabelle/bad75618fb82);Fri, Jul 24, 10:38 PM
makariusrAFP40e16c534243: much faster proofs (cf. Isabelle/bad75618fb82);Fri, Jul 24, 10:09 PM
makariusrISABELLEd3cad9ecd0cc: follow Phabricator update 2020 Week 27;Fri, Jul 24, 8:43 PM
Achim D. Brucker <adbrucker@0x5f.org>rAFP7757456aafcf: Fixed failing proofs.
Achim D. Brucker <adbrucker@0x5f.org> committed rAFP7757456aafcf: Fixed failing proofs.. 
Fri, Jul 24, 8:17 PM
makariusrISABELLEb17be02a0a11: tuned;Fri, Jul 24, 4:45 PM
makariusrISABELLE9cde8c4ea5a5: discontinued obsolete "isabelle imports" and all_known data;Fri, Jul 24, 3:37 PM
makariusrISABELLEce844442e2ab: obsolete (see 9cde8c4ea5a5);Fri, Jul 24, 3:37 PM
makariusrISABELLEebf3ba74bc4c: unused;Fri, Jul 24, 3:20 PM
makariusrISABELLE4768b1facec2: clarified errors: avoid hiding of import_errors/dir_errors by their…Fri, Jul 24, 3:02 PM
dcjmrPOLYML196ac3bc7d11: Move the test for the result of PolyCompareArbitrary up to the top-level of…Fri, Jul 24, 1:08 PM
dcjmrPOLYMLb9e4e5128d56: Merge commit '196ac3bc7d11b43f488fb945077aac162144bd31'Fri, Jul 24, 1:08 PM
Achim D. Brucker <adbrucker@0x5f.org>rAFP34a339f71b38: Added proofs about get_tag_type.
Achim D. Brucker <adbrucker@0x5f.org> committed rAFP34a339f71b38: Added proofs about get_tag_type.. 
Fri, Jul 24, 12:54 PM
dcjmrPOLYML7e214665fa88: Remove push and pop of rcx/ecx in CALL_EXTRA macro. This seems to be a relic…Fri, Jul 24, 12:39 PM