| Author | Object | Transaction | Date |
|---|
| makarius | rISABELLE2b996a0df1ce: proper clean_build of old data at start of new process --- allow to inspect… | | Mar 6 2023, 3:01 PM |
| makarius | rISABELLEfcda9a009213: more database content: formal end_build; | | Mar 6 2023, 12:08 PM |
| makarius | rISABELLE1bbf29ec9ce3: more operations; | | Mar 6 2023, 12:07 PM |
| makarius | rISABELLE7c7f1473e51a: clarified database content and prepare/init stages; | | Mar 6 2023, 11:39 AM |
| makarius | rISABELLE334a286b2975: tuned signature; | | Mar 6 2023, 10:58 AM |
| makarius | rISABELLEfc57886e37dd: tuned; | | Mar 6 2023, 10:16 AM |
| makarius | rISABELLE8f464df3520a: tuned; | | Mar 6 2023, 10:08 AM |
| makarius | rISABELLE69af424b1f9d: less verbosity, amending 3bc49507bae5; | | Mar 6 2023, 9:50 AM |
| makarius | rISABELLE3481e54bd8f1: tuned comments; | | Mar 6 2023, 9:46 AM |
| makarius | rISABELLE3362f84a300a: tuned signature: avoid totally adhoc overriding; | | Mar 6 2023, 9:37 AM |
| makarius | rISABELLE40ccee0fe19a: separate static build_uuid from dynamic worker_uuid, to allow multiple worker… | | Mar 6 2023, 9:32 AM |
| makarius | rISABELLE26ec258e5cf8: enforce rebuild of Isabelle/ML, after various changes to build database… | | Mar 5 2023, 8:41 PM |
| makarius | rISABELLE790085b1002f: more detailed table "isabelle_build_serial": allow to monitor activity of… | | Mar 5 2023, 8:41 PM |
| makarius | rISABELLEe3ed231fa214: tuned output; | | Mar 5 2023, 7:33 PM |
| makarius | rISABELLEde6fb423fd4b: clarified database content: store actual value instead of index; | | Mar 5 2023, 7:21 PM |
| makarius | rISABELLEa3dda42cd110: more robust: disallow override; | | Mar 5 2023, 6:38 PM |
| makarius | rISABELLE9398c48ea3d2: tuned messages; | | Mar 5 2023, 6:20 PM |
| makarius | rISABELLEa1d30297cd61: more complete coverage of non-final Progress methods, notably for Server. | | Mar 5 2023, 6:18 PM |
| makarius | rISABELLE5642de4d225d: clarified signature: manage "verbose" flag via "progress"; | | Mar 5 2023, 4:36 PM |
| makarius | rISABELLE84aa349ed597: removed unused arguments: avoid ambiguity concerning progress/verbose; | | Mar 5 2023, 4:26 PM |
| makarius | rISABELLE12ace037d05e: clarified protocol for "verbose" messages; | | Mar 5 2023, 4:14 PM |
| makarius | rISABELLEfda4da0f80f4: clarified signature: manage "verbose" flag via "progress"; | | Mar 5 2023, 3:34 PM |
| makarius | rISABELLEede77a627b3a: tuned; | | Mar 5 2023, 3:25 PM |
| makarius | rISABELLE71e3e144dc08: tuned; | | Mar 5 2023, 3:19 PM |
| makarius | rISABELLE6aae7486e94a: more operations; | | Mar 5 2023, 3:19 PM |
| makarius | rISABELLEacaa89cb977b: tuned signature; | | Mar 5 2023, 2:53 PM |
| makarius | rISABELLE43bfb65ee9b3: more robust: proper bound checks; | | Mar 5 2023, 1:42 PM |
| makarius | rISABELLE7d13996ffecc: proper "val verbose" (amending 2e2b2bd6b2d2); | | Mar 5 2023, 1:29 PM |
| makarius | rISABELLE2e2b2bd6b2d2: clarified signature: require just one "override def echo(message: Progress. | | Mar 5 2023, 1:29 PM |
| makarius | rISABELLE9853251b958e: enforce rebuild of Isabelle/ML, after various changes to build database… | | Mar 5 2023, 12:52 PM |
| makarius | rISABELLE3d6db917bd1b: clarified modules; | | Mar 4 2023, 11:43 PM |
| paulson <lp15@cam.ac.uk> | rAFP2859e11cc09b: Tiny bit more tidying | | Mar 4 2023, 11:39 PM |
| makarius | rISABELLEf5d6cd98b16a: clarified signature: manage "verbose" flag via "progress"; | | Mar 4 2023, 11:25 PM |
| makarius | rISABELLE3bc49507bae5: clarified treatment of "verbose" messages, e.g. Progress.theory(); | | Mar 4 2023, 10:29 PM |
| makarius | rAFPc108150a5701: more robust: allow optional arguments in isabelle.Progress.echo; | | Mar 4 2023, 9:50 PM |
| makarius | rISABELLE7d13996ffecc: proper "val verbose" (amending 2e2b2bd6b2d2); | | Mar 4 2023, 9:41 PM |
| makarius | rISABELLE8dfe2fbc98e7: tuned whitespace; | | Mar 4 2023, 9:25 PM |
| makarius | rISABELLEa8175b950173: more robust signature: avoid totally adhoc overriding (see also Build_Process. | | Mar 4 2023, 5:36 PM |
| makarius | rISABELLE7ee426daafa3: support progress backed by database; | | Mar 4 2023, 4:45 PM |
| makarius | rISABELLEfd40e36045fd: tuned; | | Mar 4 2023, 4:15 PM |
| makarius | rISABELLEdaf632e9ce7e: tuned messages; | | Mar 4 2023, 12:59 PM |
| makarius | rISABELLE2e2b2bd6b2d2: clarified signature: require just one "override def echo(message: Progress. | | Mar 4 2023, 12:43 PM |
| makarius | rISABELLE2d8815f98537: tuned signature; | | Mar 4 2023, 12:16 PM |
| makarius | rISABELLEbbb78dba6f68: tuned signature; | | Mar 4 2023, 12:14 PM |
| makarius | rISABELLE8fc94efa954a: clarified signature: more uniform Progress.verbose, avoid adhoc "override def… | | Mar 4 2023, 12:05 PM |
| makarius | rISABELLE2d12cb7ff829: proper Output.writeln_text (with clean_yxml) for all instances of Progress.echo; | | Mar 4 2023, 11:45 AM |
| makarius | rISABELLEb9e01beef1c5: merged | | Mar 3 2023, 8:11 PM |
| makarius | rISABELLEf0d9f9196b9b: more database content; | | Mar 3 2023, 8:10 PM |
| paulson <lp15@cam.ac.uk> | rAFPc4b3e385e173: More tidying | | Mar 3 2023, 5:57 PM |
| makarius | rISABELLEc546e3e1f7f6: tuned signature; | | Mar 3 2023, 1:50 PM |
| makarius | rISABELLE1a32b4928aad: tuned whitespace; | | Mar 3 2023, 1:50 PM |
| makarius | rISABELLE2d5529f56124: tuned signature; | | Mar 3 2023, 1:39 PM |
| paulson | rISABELLEfd9422c110ed: merged | | Mar 3 2023, 1:22 PM |
| paulson <lp15@cam.ac.uk> | rISABELLE9d431c939a7f: More of Eberl's material | | Mar 3 2023, 1:21 PM |
| blanchette | rISABELLE8a28ab58d155: detect duplicates in Sledgehammer output -- suggested by Larry Paulson | | Mar 3 2023, 11:25 AM |
| blanchette | rISABELLE615a6a6a4b0b: got rid of 'important message' mechanism in SystemOnTPTP (which is less used… | | Mar 3 2023, 10:30 AM |
| paulson <lp15@cam.ac.uk> | rISABELLE2c86ea8961b5: Some new lemmas. Some tidying up | | Mar 2 2023, 6:17 PM |
| makarius | rISABELLE0cebcbeac4c7: provide polyml-5.4.1 as regular component; | | Mar 2 2023, 6:15 PM |
| makarius | rISABELLE1e10689ee184: unused (see also 0cebcbeac4c7); | | Mar 2 2023, 6:15 PM |
| makarius | rISABELLEf7e413e8d269: more robust: first register job, then start job; | | Mar 2 2023, 6:15 PM |
| makarius | rISABELLEecfe6dac3a3e: simplified startup under "locked" condition (in contrast to f7e413e8d269); | | Mar 2 2023, 6:15 PM |
| makarius | rISABELLE4fec9413f14b: identify Build_Process.Context.instance with Sessions.Build_Info (see also… | | Mar 2 2023, 6:15 PM |
| makarius | rISABELLEff164add75cd: maintain "uuid" column in session build database, to identity the original… | | Mar 2 2023, 6:15 PM |
| makarius | rISABELLE0c704aba71e3: clarified signature: reduce explicit access to static Sessions.Structure; | | Mar 2 2023, 6:15 PM |
| makarius | rISABELLE566e6e393126: proper deps from build_graph, not imports_graph (amending 0c704aba71e3); | | Mar 2 2023, 6:15 PM |
| makarius | rISABELLE57ede1743caf: merged | | Mar 2 2023, 5:46 PM |
| makarius | rISABELLE032c76e04475: clarified execution context: main work happens within Future.thread; | | Mar 2 2023, 5:05 PM |
| makarius | rISABELLE911d3dbf2033: clarified timeout: closer to actual process; | | Mar 2 2023, 4:39 PM |
| makarius | rISABELLE7ba474a01249: tuned names; | | Mar 2 2023, 4:24 PM |
| makarius | rISABELLE291f5848bf55: clarified names; | | Mar 2 2023, 4:09 PM |
| makarius | rISABELLE10147ecf9196: tuned, following ML_Statistics.monitor; | | Mar 2 2023, 3:55 PM |
| makarius | rISABELLE1e10689ee184: unused (see also 0cebcbeac4c7); | | Mar 2 2023, 3:51 PM |
| makarius | rISABELLE1082f0d6628b: tuned; | | Mar 2 2023, 3:39 PM |
| makarius | rISABELLEabc9706a4ca2: tuned; | | Mar 2 2023, 3:39 PM |
| makarius | rISABELLEe50cad69cbe7: tuned comments; | | Mar 2 2023, 3:04 PM |
| paulson | rAFP5818f34777c7: Rensets metadata | | Mar 2 2023, 2:59 PM |
| paulson <lp15@cam.ac.uk> | rAFP838da7313b56: New entry Rensets | | Mar 2 2023, 2:59 PM |
| makarius | rISABELLEf376aebca9c1: clarified modules; | | Mar 2 2023, 2:58 PM |
| makarius | rISABELLE5f6f567a2661: clarified modules; | | Mar 2 2023, 2:41 PM |
| makarius | rISABELLE3bc611c80346: clarified modules; | | Mar 2 2023, 2:22 PM |
| makarius | rISABELLE5ecaf881b563: clarified signature; | | Mar 2 2023, 1:26 PM |
| makarius | rISABELLE362bf802013e: clarified modules; | | Mar 2 2023, 1:19 PM |
| paulson | rAFP00ea0edc8e9c: merged | | Mar 2 2023, 12:47 PM |
| paulson <lp15@cam.ac.uk> | rAFP15aa85454af5: Suppression of duplicate syntax for abs_summable_on, etc. | | Mar 2 2023, 12:47 PM |
| paulson | rISABELLEdf1150ec6cd7: merged | | Mar 2 2023, 12:34 PM |
| makarius | rISABELLEa073ac3f3b56: clarified modules; | | Mar 2 2023, 11:36 AM |
| makarius | rISABELLE50488bcd99f6: tuned; | | Mar 2 2023, 11:25 AM |
| makarius | rISABELLE38503d9ff2e5: clarified modules; | | Mar 2 2023, 11:19 AM |
| paulson <lp15@cam.ac.uk> | rAFPeaee624276bb: No more sorted_take, sorted_drop | | Mar 2 2023, 11:15 AM |
| makarius | rISABELLE5af7e8ffcab7: clarified modules; | | Mar 2 2023, 11:11 AM |
| makarius | rISABELLEed292479eaa9: tuned; | | Mar 1 2023, 10:22 PM |
| makarius | rISABELLEe27bc7957297: more robust: proper synchronization of transition from next_job to… | | Mar 1 2023, 10:06 PM |
| paulson <lp15@cam.ac.uk> | rISABELLE5b3139a6b0de: A little bit more tidying up | | Mar 1 2023, 10:05 PM |
| makarius | rISABELLE94dcf2c3895a: more thorough synchronized_database for internal *and* external state; | | Mar 1 2023, 9:53 PM |
| makarius | rISABELLEecfe6dac3a3e: simplified startup under "locked" condition (in contrast to f7e413e8d269); | | Mar 1 2023, 9:24 PM |
| makarius | rISABELLE8008ce0f2488: more explicit session name, in anticipation of variants like "session.document"… | | Mar 1 2023, 9:15 PM |
| makarius | rISABELLE4e8bec105ce5: tuned signature; | | Mar 1 2023, 9:07 PM |
| makarius | rISABELLEb474d39ddfee: tuned signature; | | Mar 1 2023, 9:04 PM |
| makarius | rISABELLEa553e419e9dc: tuned signature; | | Mar 1 2023, 8:59 PM |
| makarius | rISABELLEccca589d7027: tuned signature: support general Build_Job instances; | | Mar 1 2023, 8:47 PM |