Page MenuHomeIsabelle/Phabricator
Feed All Stories

Today

makarius committed rISABELLE16fab31feadc: avoid failure of "isabelle build -o skip_proofs";.
avoid failure of "isabelle build -o skip_proofs";
Fri, Aug 7, 11:49 AM
makarius committed rISABELLEae683a461c40: merged.
merged
Fri, Aug 7, 12:09 AM
makarius committed rISABELLE411b3dc036ca: recovered stderr for PIDE batch-build, such as "Browser info at ...", "Document….
recovered stderr for PIDE batch-build, such as "Browser info at ...", "Document…
Fri, Aug 7, 12:09 AM
makarius committed rISABELLE1b06ed254943: more compact command_timings, as in former batch-build;.
more compact command_timings, as in former batch-build;
Fri, Aug 7, 12:09 AM
makarius committed rISABELLE36743e0e2c4c: unused;.
unused;
Fri, Aug 7, 12:09 AM
makarius committed rISABELLEa1fb4d28e609: unused --- superseded by PIDE messages;.
unused --- superseded by PIDE messages;
Fri, Aug 7, 12:09 AM
makarius committed rISABELLEd9a42786fbc9: more thorough cleanup, e.g. before ML_Heap.save;.
more thorough cleanup, e.g. before ML_Heap.save;
Fri, Aug 7, 12:09 AM
makarius committed rISABELLE7b318273a4aa: discontinued old batch-build functionality;.
discontinued old batch-build functionality;
Fri, Aug 7, 12:09 AM

Yesterday

florian.haftmann committed rAFP116a82414c28: dropped alias.
dropped alias
Thu, Aug 6, 11:05 PM
florian.haftmann committed rISABELLE0b21b2beadb5: tailored towards remaining essence.
tailored towards remaining essence
Thu, Aug 6, 11:05 PM
dcjm committed rPOLYML59232968ed60: Posix.Process.exit should call PolyFinish rather than PolyTerminate so that… (authored by dcjm).
Posix.Process.exit should call PolyFinish rather than PolyTerminate so that…
Thu, Aug 6, 6:14 PM
dcjm committed rPOLYMLe51f00cccb0a: Tidy-up shutdown of statistics. (authored by dcjm).
Tidy-up shutdown of statistics.
Thu, Aug 6, 6:14 PM
dcjm committed rPOLYMLcbd49e8ae6cd: Fix changes to statistics.cpp for Windows. (authored by dcjm).
Fix changes to statistics.cpp for Windows.
Thu, Aug 6, 6:14 PM
dcjm committed rPOLYMLc1ff455836c7: Unlink any existing statistics file. Open will fail if it exists. Report an… (authored by dcjm).
Unlink any existing statistics file. Open will fail if it exists. Report an…
Thu, Aug 6, 6:14 PM
nipkow committed rISABELLEc65614b556b2: merged.
merged
Thu, Aug 6, 5:51 PM
nipkow committed rISABELLEf978ecaf119a: added theory Tree23_of_List.
added theory Tree23_of_List
Thu, Aug 6, 5:51 PM
nipkow committed rISABELLE9fa6dde8d959: tuned.
tuned
Thu, Aug 6, 5:51 PM
makarius committed rISABELLE8c547eac8381: more robust treatment of thm_names, with strict check after all theories are….
more robust treatment of thm_names, with strict check after all theories are…
Thu, Aug 6, 5:31 PM
paulson <lp15@cam.ac.uk> committed rISABELLE496cfe488d72: a few more lemmas.
a few more lemmas
Thu, Aug 6, 3:54 PM
dcjm committed rPOLYML4c21a9d8e5e7: Small change to 8e4d341 to allow compilation when int is IntInf.int. (authored by dcjm).
Small change to 8e4d341 to allow compilation when int is IntInf.int.
Thu, Aug 6, 8:40 AM
paulson committed rISABELLE6b5421bd0fc3: merged.
merged
Thu, Aug 6, 12:26 AM
paulson <lp15@cam.ac.uk> committed rISABELLEbeccb2a0410f: yet another little lemma.
yet another little lemma
Thu, Aug 6, 12:26 AM
paulson <lp15@cam.ac.uk> committed rISABELLEcfb6c22a5636: lemmas about sets and the enumerate operator.
lemmas about sets and the enumerate operator
Thu, Aug 6, 12:26 AM
paulson committed rISABELLE6a2f43901350: merged.
merged
Thu, Aug 6, 12:26 AM
paulson committed rISABELLE3f8e6c0166ac: merged.
merged
Thu, Aug 6, 12:26 AM
paulson committed rISABELLEb6065cbbf5e2: merged.
merged
Thu, Aug 6, 12:26 AM
paulson <lp15@cam.ac.uk> committed rISABELLE5d17e7a0825a: strengthened a lemma.
strengthened a lemma
Thu, Aug 6, 12:26 AM
paulson <lp15@cam.ac.uk> committed rISABELLE8348bba699e6: A new lemma about abstract Sum / Prod.
A new lemma about abstract Sum / Prod
Thu, Aug 6, 12:26 AM

Wed, Aug 5

florian.haftmann committed rISABELLEa36db1c8238e: separation of reversed bit lists from other material.
separation of reversed bit lists from other material
Wed, Aug 5, 7:07 PM
florian.haftmann committed rAFP3e79743d7844: separation of reversed bit lists from other material.
separation of reversed bit lists from other material
Wed, Aug 5, 7:07 PM
makarius committed rISABELLE43a43b182a81: merged.
merged
Wed, Aug 5, 6:46 PM
makarius committed rISABELLE41e1e2395a67: avoid exhaustion of worker threads, notably due to complex interaction of….
avoid exhaustion of worker threads, notably due to complex interaction of…
Wed, Aug 5, 6:46 PM
makarius committed rISABELLE3afd6b1c7ab5: more robust: insist in finished future;.
more robust: insist in finished future;
Wed, Aug 5, 6:46 PM
makarius committed rISABELLEdf99d26efeeb: unused;.
unused;
Wed, Aug 5, 6:46 PM
florian.haftmann committed rAFPcac1c67360f3: further refinement of code equations for mask operation.
further refinement of code equations for mask operation
Wed, Aug 5, 1:05 PM
florian.haftmann committed rISABELLE3ec876181527: further refinement of code equations for mask operation.
further refinement of code equations for mask operation
Wed, Aug 5, 1:05 PM

Tue, Aug 4

florian.haftmann committed rISABELLE41393ecb57ac: uniform mask operation.
uniform mask operation
Tue, Aug 4, 3:26 PM
florian.haftmann committed rISABELLEe4d42f5766dc: clearer separation of pre-word bit list material.
clearer separation of pre-word bit list material
Tue, Aug 4, 3:25 PM
florian.haftmann committed rAFPf28d68deefa8: uniform mask operation.
uniform mask operation
Tue, Aug 4, 3:25 PM
florian.haftmann committed rAFP52ddcd32c0c9: clearer separation of pre-word bit list material.
clearer separation of pre-word bit list material
Tue, Aug 4, 3:25 PM
florian.haftmann committed rAFP9b629e0e6654: repaired document slip.
repaired document slip
Tue, Aug 4, 7:22 AM

Mon, Aug 3

nipkow committed rISABELLE2030eacf3a72: added lemma.
added lemma
Mon, Aug 3, 4:23 PM

Sat, Aug 1

florian.haftmann committed rAFPef3c8932106a: more consequent transferability.
more consequent transferability
Sat, Aug 1, 9:18 PM
florian.haftmann committed rISABELLE8c355e2dd7db: more consequent transferability.
more consequent transferability
Sat, Aug 1, 8:55 PM

Thu, Jul 30

dcjm committed rPOLYMLd471c5e6e1cf: Update compiler version to 5.8.2 so that we pick up the correct files on… (authored by dcjm).
Update compiler version to 5.8.2 so that we pick up the correct files on…
Thu, Jul 30, 1:46 PM
dcjm committed rPOLYML8e4d341bd778: Check inside the simplifier that the body of a potential inline function is… (authored by dcjm).
Check inside the simplifier that the body of a potential inline function is…
Thu, Jul 30, 1:46 PM
dcjm committed rPOLYML6442ac3a51c6: Remove unused parameters. (authored by dcjm).
Remove unused parameters.
Thu, Jul 30, 1:46 PM
dcjm committed rPOLYML654e1adee079: Merge branch 'master' of github.com:dcjm/polyml (authored by dcjm).
Merge branch 'master' of github.com:dcjm/polyml
Thu, Jul 30, 1:46 PM
dcjm committed rPOLYML5dc69bc3a7d5: Search for machine/reloc.h separately from elf_abi.h. These seem to have been… (authored by dcjm).
Search for machine/reloc.h separately from elf_abi.h. These seem to have been…
Thu, Jul 30, 1:46 PM
dcjm committed rPOLYML7d72f11eeab9: Change all the casts from PolyWord* to stackItem*. Some had been missed. (authored by dcjm).
Change all the casts from PolyWord* to stackItem*. Some had been missed.
Thu, Jul 30, 1:46 PM

Wed, Jul 29

makarius committed rISABELLEb8d0b8659e0a: more robust scheduler shutdown, notably for spurious crashes;.
more robust scheduler shutdown, notably for spurious crashes;
Wed, Jul 29, 8:46 PM

Mon, Jul 27

nipkow committed rISABELLE1d6c3cba47fe: unclear why I ever asked for type tree2.
unclear why I ever asked for type tree2
Mon, Jul 27, 3:59 PM

Sun, Jul 26

makarius committed rISABELLEbd9d1ce274c9: enforce pide_session to see if all isabelle_cronjob tasks work smoothly with it;.
enforce pide_session to see if all isabelle_cronjob tasks work smoothly with it;
Sun, Jul 26, 10:39 PM
makarius committed rISABELLE9c0b835d4cc2: proper pretty printing for latex output, notably for pide_session=true….
proper pretty printing for latex output, notably for pide_session=true…
Sun, Jul 26, 10:39 PM

Sat, Jul 25

makarius committed rISABELLEf3e1144a1cec: clarified name to avoid duplication (no distinction of data on host =….
clarified name to avoid duplication (no distinction of data on host =…
Sat, Jul 25, 11:27 PM
makarius committed rISABELLEf56522a44564: clarified names;.
clarified names;
Sat, Jul 25, 11:27 PM
makarius committed rISABELLEfed7b0ae20d8: more errors;.
more errors;
Sat, Jul 25, 12:49 PM

Fri, Jul 24

makarius committed rAFP40e16c534243: much faster proofs (cf. Isabelle/bad75618fb82);.
much faster proofs (cf. Isabelle/bad75618fb82);
Fri, Jul 24, 10:38 PM
makarius committed rISABELLEd3cad9ecd0cc: follow Phabricator update 2020 Week 27;.
follow Phabricator update 2020 Week 27;
Fri, Jul 24, 8:47 PM
makarius committed rISABELLEb17be02a0a11: tuned;.
tuned;
Fri, Jul 24, 8:47 PM
Achim D. Brucker <adbrucker@0x5f.org> committed rAFP7757456aafcf: Fixed failing proofs..
Fixed failing proofs.
Fri, Jul 24, 8:18 PM
makarius committed rISABELLEebf3ba74bc4c: unused;.
unused;
Fri, Jul 24, 3:37 PM
makarius committed rISABELLE4768b1facec2: clarified errors: avoid hiding of import_errors/dir_errors by their….
clarified errors: avoid hiding of import_errors/dir_errors by their…
Fri, Jul 24, 3:37 PM
makarius committed rISABELLEba5b37671528: clarified signature;.
clarified signature;
Fri, Jul 24, 3:37 PM
makarius committed rISABELLE17507b48b6f5: clarified errors: avoid accidental import from other session that happens to be….
clarified errors: avoid accidental import from other session that happens to be…
Fri, Jul 24, 3:37 PM
makarius committed rISABELLE11dc8929832d: clarified order --- proper sorting of requirements;.
clarified order --- proper sorting of requirements;
Fri, Jul 24, 3:37 PM
makarius committed rISABELLEce844442e2ab: obsolete (see 9cde8c4ea5a5);.
obsolete (see 9cde8c4ea5a5);
Fri, Jul 24, 3:37 PM
makarius committed rISABELLE25985d757b0a: tuned --- based on hints by IntelliJ;.
tuned --- based on hints by IntelliJ;
Fri, Jul 24, 3:37 PM
makarius committed rISABELLEd0909b5d88eb: tuned signature;.
tuned signature;
Fri, Jul 24, 3:37 PM
Achim D. Brucker <adbrucker@0x5f.org> committed rAFP226cc9fd1567: Mostly improving theory format (adding line breaks) and added.
Mostly improving theory format (adding line breaks) and added
Fri, Jul 24, 1:42 PM
Achim D. Brucker <adbrucker@0x5f.org> committed rAFP34a339f71b38: Added proofs about get_tag_type..
Added proofs about get_tag_type.
Fri, Jul 24, 1:42 PM
dcjm committed rPOLYML7e214665fa88: Remove push and pop of rcx/ecx in CALL_EXTRA macro. This seems to be a relic… (authored by dcjm).
Remove push and pop of rcx/ecx in CALL_EXTRA macro. This seems to be a relic…
Fri, Jul 24, 1:08 PM
dcjm committed rPOLYMLb9e4e5128d56: Merge commit '196ac3bc7d11b43f488fb945077aac162144bd31' (authored by dcjm).
Merge commit '196ac3bc7d11b43f488fb945077aac162144bd31'
Fri, Jul 24, 1:08 PM
dcjm committed rPOLYML196ac3bc7d11: Move the test for the result of PolyCompareArbitrary up to the top-level of… (authored by dcjm).
Move the test for the result of PolyCompareArbitrary up to the top-level of…
Fri, Jul 24, 1:08 PM
dcjm committed rPOLYMLf186be011f67: Add PointerEq as a binary operation and reserve WordComparison for the tagged… (authored by dcjm).
Add PointerEq as a binary operation and reserve WordComparison for the tagged…
Fri, Jul 24, 1:08 PM

Tue, Jul 21

makarius committed rISABELLE0f2ff88f823e: updated to polyml-5.8.1 (official release);.
updated to polyml-5.8.1 (official release);
Tue, Jul 21, 1:12 PM
makarius triaged T22: Discontinue obsolete Theory_Data.extend as Low priority.
Tue, Jul 21, 12:52 PM
dcjm committed rPOLYML382ffb7801c2: Merge branch 'master' into GCPercent (authored by dcjm).
Merge branch 'master' into GCPercent
Tue, Jul 21, 9:54 AM
dcjm committed rPOLYML2fdff98984e6: Add Unix socket test. This was added in another branch. (authored by dcjm).
Add Unix socket test. This was added in another branch.
Tue, Jul 21, 9:54 AM

Mon, Jul 20

makarius created Blog Post: Theory_Data extend operation is obsolete and needs to be the identity function.
Mon, Jul 20, 11:59 PM
makarius committed rISABELLEefb7fd4a6d1f: subtle change of Theory_Data extend/merge semantics due to Theory.join_theory;.
subtle change of Theory_Data extend/merge semantics due to Theory.join_theory;
Mon, Jul 20, 11:58 PM
dcjm committed rPOLYML15aba84a490d: Added Weak.touch to Weak structure documentation. (authored by dcjm).
Added Weak.touch to Weak structure documentation.
Mon, Jul 20, 11:57 PM
makarius committed rAFPc02eaed866dc: data extend is obsolete and should be identity;.
data extend is obsolete and should be identity;
Mon, Jul 20, 11:51 PM
dcjm committed rPOLYML8d0dc1c68328: Updated pre-built compilers for 64-bit amd 32-in-64 Windows. (authored by dcjm).
Updated pre-built compilers for 64-bit amd 32-in-64 Windows.
Mon, Jul 20, 5:47 PM
dcjm committed rPOLYML5d4bfda79793: Rebuild pre-built compilers for 64-bit SysV, 32-in-64 SysV and 64-bit… (authored by dcjm).
Rebuild pre-built compilers for 64-bit SysV, 32-in-64 SysV and 64-bit…
Mon, Jul 20, 5:46 PM
dcjm committed rPOLYMLba0fcdf61920: Updated pre-built compilers for 32-bit native X86 and interpreted versions. (authored by dcjm).
Updated pre-built compilers for 32-bit native X86 and interpreted versions.
Mon, Jul 20, 5:46 PM
dcjm committed rPOLYML6841e8bc8bd1: Rebuild configure with new release numbers. (authored by dcjm).
Rebuild configure with new release numbers.
Mon, Jul 20, 5:46 PM
dcjm committed rPOLYML382085c5f04c: Update version numbers ready for release of 5.8.1. (authored by dcjm).
Update version numbers ready for release of 5.8.1.
Mon, Jul 20, 5:46 PM

Fri, Jul 17

makarius committed rISABELLE69880fdc8310: clarified -- avoid non-standard extend/merge;.
clarified -- avoid non-standard extend/merge;
Fri, Jul 17, 9:52 PM
makarius committed rISABELLEce3f26b4e790: clarified -- avoid non-standard extend/merge;.
clarified -- avoid non-standard extend/merge;
Fri, Jul 17, 9:51 PM
makarius committed rISABELLEf8d28617ea08: tuned -- avoid non-standard extend;.
tuned -- avoid non-standard extend;
Fri, Jul 17, 9:51 PM
makarius committed rISABELLEb9f5f30b623f: proper session imports;.
proper session imports;
Fri, Jul 17, 9:51 PM
makarius committed rISABELLEdeb390860f07: clarified -- avoid non-standard extend;.
clarified -- avoid non-standard extend;
Fri, Jul 17, 9:51 PM
makarius committed rISABELLE6c75287276d5: tuned -- avoid non-standard extend/merge;.
tuned -- avoid non-standard extend/merge;
Fri, Jul 17, 9:51 PM
makarius committed rISABELLE4ed33ea8d957: prefer conservative extend/merge of theory naming;.
prefer conservative extend/merge of theory naming;
Fri, Jul 17, 9:51 PM

Thu, Jul 16

makarius committed rISABELLE912f13865596: support native PID for ML process;.
support native PID for ML process;
Thu, Jul 16, 10:55 PM
makarius committed rISABELLE438adb97d82c: merged.
merged
Thu, Jul 16, 10:55 PM
makarius committed rISABELLE18d35be9493f: proper import sessions;.
proper import sessions;
Thu, Jul 16, 10:55 PM
makarius committed rISABELLEd3b8c8b2d1fc: more thorough extend/merge (for Theory.join_theory);.
more thorough extend/merge (for Theory.join_theory);
Thu, Jul 16, 10:55 PM
makarius committed rISABELLEd4de7e4754d2: clarified theory data: more robust merge;.
clarified theory data: more robust merge;
Thu, Jul 16, 10:55 PM