| Author | Object | Transaction | Date |
|---|
| makarius | rISABELLE40b5ee5889d2: clarified management of services: static declarations vs. dynamic instances (e. | | Aug 16 2020, 11:57 AM |
| makarius | rISABELLE065dcd80293e: provide protocol handlers via isabelle_system_service; | | Aug 15 2020, 10:07 PM |
| makarius | rISABELLEcafe00f2161e: proper protocol init (amending 065dcd80293e); | | Aug 15 2020, 10:07 PM |
| makarius | rISABELLEcafe00f2161e: proper protocol init (amending 065dcd80293e); | | Aug 15 2020, 1:51 PM |
| makarius | rISABELLEd1ca82e27cbc: clarified names; | | Aug 15 2020, 1:45 PM |
| makarius | rISABELLE065dcd80293e: provide protocol handlers via isabelle_system_service; | | Aug 15 2020, 1:37 PM |
| makarius | rISABELLE837b86b214d3: prefer formal name; | | Aug 15 2020, 1:36 PM |
| makarius | rISABELLE2b41b710f6ef: clarified signature; | | Aug 14 2020, 5:14 PM |
| makarius | rAFPa067d7a7ff67: clarified signature (see Isabelle/2b41b710f6ef); | | Aug 14 2020, 5:14 PM |
| pruvisto | rAFP6e56f286a19f: sitegen for Amicable_Numbers | | Aug 14 2020, 4:42 PM |
| pruvisto | rAFP4bc297a7a99a: New entry: Amicable_Numbers | | Aug 14 2020, 4:42 PM |
| makarius | rAFPa067d7a7ff67: clarified signature (see Isabelle/2b41b710f6ef); | | Aug 14 2020, 3:02 PM |
| makarius | rISABELLE2b41b710f6ef: clarified signature; | | Aug 14 2020, 2:40 PM |
| makarius | rISABELLEbdbd6ff5fd0b: misc tuning; | | Aug 14 2020, 2:25 PM |
| makarius | rISABELLE3fa75db844f5: clarified demo functions; | | Aug 14 2020, 1:59 PM |
| makarius | rISABELLE64df1e514005: clarified protocol: ML worker thread blocks and awaits result from Scala, to… | | Aug 14 2020, 1:26 PM |
| dcjm | rPOLYML3365cf05afda: XWindows: Replace the two calls to process_may_block by direct calls to… | | Aug 14 2020, 1:20 PM |
| Joshua Schneider <joshua.schneider@inf.ethz.ch> | rAFPd31906039242: reduced redundancy by sharing theories with MFOTL_Monitor; | | Aug 14 2020, 8:27 AM |
| Joshua Schneider <joshua.schneider@inf.ethz.ch> | rAFP3c4396a19260: MFOTL_Monitor change history | | Aug 13 2020, 5:23 PM |
| Joshua Schneider <joshua.schneider@inf.ethz.ch> | rAFPb1639ed541b7: added abstract slicing framework to MFOTL_Monitor; | | Aug 13 2020, 5:11 PM |
| makarius | Blog Post: Improved monitoring for Isabelle/ML and Java | | Aug 13 2020, 4:22 PM |
| makarius | Blog Post: Improved monitoring for Isabelle/ML and Java | makarius renamed this blog post from to Isabelle/jEdit Prover IDE: improved monitoring for Isabelle/ML and Java. | Aug 13 2020, 4:22 PM |
| makarius | Blog Post: Improved monitoring for Isabelle/ML and Java | | Aug 13 2020, 4:22 PM |
| makarius | Blog Post: Improved monitoring for Isabelle/ML and Java | makarius set this post's subtitle to "". | Aug 13 2020, 4:22 PM |
| makarius | Blog Post: Improved monitoring for Isabelle/ML and Java | | Aug 13 2020, 4:22 PM |
| makarius | rISABELLE510ebf846696: more documentation; | | Aug 13 2020, 3:52 PM |
| makarius | rISABELLE36a34f3a8cb8: support JVM runtime statistics; | | Aug 13 2020, 3:11 PM |
| makarius | rISABELLEd2dc9bc3a3e1: clarified worker threads; | | Aug 13 2020, 2:41 PM |
| makarius | rISABELLE2375b38a42f8: misc tuning, based on hints by IntelliJ IDEA; | | Aug 13 2020, 1:18 PM |
| makarius | rISABELLEd8dd3aa6dae9: clarified GUI; | | Aug 13 2020, 1:13 PM |
| makarius | rISABELLE25db9c4209ee: tuned GUI; | | Aug 13 2020, 12:59 PM |
| makarius | rISABELLE6a4e51ca53c3: tuned GUI; | | Aug 13 2020, 12:53 PM |
| makarius | rISABELLE4a46650bf701: clarified order for GUI; | | Aug 13 2020, 12:38 PM |
| makarius | rISABELLE6e8b5cdd4ba0: tuned; | | Aug 13 2020, 12:33 PM |
| makarius | rISABELLE262d3c11a24d: clarified GUI; | | Aug 13 2020, 12:29 PM |
| makarius | rISABELLEf67e83608745: removed pointless GUI controls for ML_statistics --- no longer part of prover… | | Aug 12 2020, 8:33 PM |
| makarius | rISABELLE38a64cc17403: GUI controls for ML_statistics, for more digestible protocol dump; | | Aug 12 2020, 8:33 PM |
| makarius | rISABELLEae6544cf1c8c: show GC progress as "ML cleanup"; | | Aug 12 2020, 8:09 PM |
| makarius | rISABELLEf5c085dfa02f: ML status widget similar to org.gjt.sp.jedit.gui.statusbar. | | Aug 12 2020, 7:34 PM |
| makarius | rISABELLEfa57d299b46b: support for Poly/ML memory status; | | Aug 12 2020, 7:32 PM |
| dcjm | rPOLYML8e316fd16edd: Remove the code to make trampolines since they are no longer used. | | Aug 12 2020, 7:00 PM |
| dcjm | rPOLYML3d031d25a475: Merge branch 'CompileForeignCall' into CompliedFFITesting | | Aug 12 2020, 6:55 PM |
| dcjm | rPOLYML04a4c1ed1756: Merge branch 'master' into AnotherPollBranch | | Aug 12 2020, 6:25 PM |
| makarius | rISABELLEad277a335aa5: clarified signature; | | Aug 12 2020, 5:53 PM |
| makarius | rISABELLE98dca728fc9c: removed pointless option "ML_statistics": always enabled; | | Aug 12 2020, 11:26 AM |
| makarius | rISABELLEf67e83608745: removed pointless GUI controls for ML_statistics --- no longer part of prover… | | Aug 12 2020, 11:22 AM |
| makarius | rISABELLEf40200b5bb3c: support for GC state; | | Aug 12 2020, 11:07 AM |
| makarius | rISABELLEc500f6c86e86: updated to polyml-test-f54aa41240d0; | | Aug 11 2020, 7:01 PM |
| dcjm | rPOLYMLf54aa41240d0: Functions marked as InlineAlways can be recursive and so the inline marking has… | | Aug 11 2020, 5:07 PM |
| dcjm | rPOLYMLf28c1f2d462c: Use config.h for the Windows osmem if it is provided e.g. by Msys. | | Aug 11 2020, 3:09 PM |
| makarius | rISABELLEd756ff4bb3a3: back to polyml-5.8.1 due to ML compiler crash in HOL-Codegenerator_Test; | | Aug 11 2020, 2:21 PM |
| makarius | rISABELLE284d6c06cbfb: updated to polyml-test-159dc81efc3b; | | Aug 11 2020, 1:15 PM |
| dcjm | rPOLYMLb95a85ead3ae: Remake Makefile.in after merge. | | Aug 11 2020, 8:54 AM |
| dcjm | rPOLYML188ea5272621: Merge branch 'ExecuteWrite' | | Aug 11 2020, 8:51 AM |
| florian.haftmann | rAFP9a9bc053eb71: dedicated symbols for code generation, to pave way for generic conversions from… | | Aug 10 2020, 5:34 PM |
| florian.haftmann | rISABELLE9e5862223442: dedicated symbols for code generation, to pave way for generic conversions from… | | Aug 10 2020, 5:34 PM |
| florian.haftmann | rISABELLE9e0321263eb3: consolidated names | | Aug 10 2020, 8:27 AM |
| florian.haftmann | rISABELLE3707cf7b370b: reduced prominence od theory Bits_Int | | Aug 10 2020, 8:27 AM |
| paulson | rAFP7950cea20592: merged | | Aug 9 2020, 8:43 PM |
| paulson <lp15@cam.ac.uk> | rAFP633328cc6a47: more on order types | | Aug 9 2020, 8:42 PM |
| paulson <lp15@cam.ac.uk> | rISABELLEa0768f16bccd: one last lemma about Total and Restr | | Aug 9 2020, 5:09 PM |
| dcjm | rPOLYMLd3b1b22f3b26: Remove ProcessExternal::SetSingleThreaded since this is handled by RtsModule… | | Aug 9 2020, 5:00 PM |
| dcjm | rPOLYML958394264734: Add a virtual function to the RtsModules class to handle the very specific case… | | Aug 9 2020, 4:50 PM |
| paulson <lp15@cam.ac.uk> | rISABELLE5de9a5fbf2ec: adjustments for fewer WO assumptions | | Aug 9 2020, 4:18 PM |
| paulson <lp15@cam.ac.uk> | rISABELLEcf8399df4d76: elimination of some needless assumptions | | Aug 9 2020, 2:18 PM |
| paulson | rISABELLE36220b07c047: merged | | Aug 9 2020, 1:51 PM |
| nipkow | rISABELLE2dcb6523f6af: tuned | | Aug 8 2020, 6:20 PM |
| nipkow | rISABELLE42f931a68856: tuned | | Aug 8 2020, 6:04 PM |
| paulson <lp15@cam.ac.uk> | rISABELLE53b724b87eb3: iso lemmas | | Aug 8 2020, 5:15 PM |
| dcjm | rPOLYML159dc81efc3b: Merge branch 'master' into GCPercent | | Aug 8 2020, 9:50 AM |
| dcjm | rPOLYMLe7e445063615: Mark inline shim functions generated by the optimiser differently from those… | | Aug 8 2020, 9:48 AM |
| dcjm | rPOLYML8e4d341bd778: Check inside the simplifier that the body of a potential inline function is… | | Aug 8 2020, 9:48 AM |
| dcjm | rPOLYML4de69b686011: Add Phil's test as a regression test. | | Aug 8 2020, 9:47 AM |
| dcjm | rPOLYMLe7e445063615: Mark inline shim functions generated by the optimiser differently from those… | | Aug 8 2020, 9:46 AM |
| makarius | rISABELLE2831933195ef: NEWS; | | Aug 7 2020, 11:33 PM |
| makarius | Blog Post: ML statistics via an external Poly/ML process | makarius set this post's subtitle to "". | Aug 7 2020, 11:33 PM |
| makarius | Blog Post: ML statistics via an external Poly/ML process | | Aug 7 2020, 11:33 PM |
| makarius | Blog Post: ML statistics via an external Poly/ML process | | Aug 7 2020, 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. | Aug 7 2020, 11:33 PM |
| makarius | Blog Post: ML statistics via an external Poly/ML process | | Aug 7 2020, 11:33 PM |
| makarius | Blog Post: ML statistics via an external Poly/ML process | | Aug 7 2020, 11:33 PM |
| makarius | rPOLYML52881757b127: The shared memory file for remote statistics on Unix is now in $POLYSTATSDIR if… | | Aug 7 2020, 11:32 PM |
| makarius | rISABELLEd115d50a19c0: provide POLYSTATSDIR to keep $HOME/.polyml clean (requires Poly/ML 52881757b127… | | Aug 7 2020, 11:32 PM |
| makarius | rISABELLE7b318273a4aa: discontinued old batch-build functionality; | | Aug 7 2020, 11:32 PM |
| makarius | rISABELLE84f716e72fa3: adapted to 7b318273a4aa; | | Aug 7 2020, 11:32 PM |
| makarius | rISABELLE2831933195ef: NEWS; | | Aug 7 2020, 11:01 PM |
| makarius | rISABELLEd115d50a19c0: provide POLYSTATSDIR to keep $HOME/.polyml clean (requires Poly/ML 52881757b127… | | Aug 7 2020, 10:57 PM |
| makarius | rISABELLE84f716e72fa3: adapted to 7b318273a4aa; | | Aug 7 2020, 10:28 PM |
| makarius | rISABELLE4d8b3209dae3: cache props; | | Aug 7 2020, 10:23 PM |
| makarius | rISABELLE7773ec172572: clarified names; | | Aug 7 2020, 10:19 PM |
| makarius | rISABELLEc998827f1df9: more thorough protocol_handlers.exit, like file_formats.stop_session; | | Aug 7 2020, 9:21 PM |
| makarius | rISABELLEd00220799735: tuned names; | | Aug 7 2020, 9:02 PM |
| makarius | rISABELLE2d9e40cfe9af: temporary workaround for 100% CPU usage in OS.Process.sleep; | | Aug 7 2020, 8:28 PM |
| makarius | rISABELLE3546dd4ade74: ML statistics via external process: allows monitoring RTS while ML program… | | Aug 7 2020, 8:19 PM |
| dcjm | rPOLYMLd57a84907afa: Poll should still pause if there are no descriptors. Fix problem with OS. | | Aug 7 2020, 8:04 PM |
| dcjm | rPOLYMLf80d20c14967: Some clean up of remote statistics in Windows. | | Aug 7 2020, 5:39 PM |
| dcjm | rPOLYML52881757b127: The shared memory file for remote statistics on Unix is now in $POLYSTATSDIR if… | | Aug 7 2020, 4:12 PM |
| makarius | rISABELLEb9ded33bd58c: clarified catch-all handler --- avoid confusion of Interrupt vs. Exn.Interrupt… | | Aug 7 2020, 3:13 PM |
| makarius | rISABELLE16fab31feadc: avoid failure of "isabelle build -o skip_proofs"; | | Aug 7 2020, 11:46 AM |
| makarius | rISABELLE940195fbb282: clarified messages; | | Aug 7 2020, 12:09 AM |