Page MenuHomeIsabelle/Phabricator
Feed All Stories

Today

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

Yesterday

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
makarius committed rISABELLE2c7cfd2f9b6c: more thorough extend/merge, notably for master_dir across Theory.join_theory (e..
more thorough extend/merge, notably for master_dir across Theory.join_theory (e.
Thu, Jul 16, 10:55 PM
makarius committed rISABELLEefd169aed4dc: more robust: avoid potential problems with encoding of directory name;.
more robust: avoid potential problems with encoding of directory name;
Thu, Jul 16, 10:55 PM
makarius committed rISABELLEc386d1b77762: more thorough extend/merge (for Theory.join_theory);.
more thorough extend/merge (for Theory.join_theory);
Thu, Jul 16, 10:55 PM
makarius committed rISABELLEb9e9ff3a1e1c: more thorough extend/merge (for Theory.join_theory);.
more thorough extend/merge (for Theory.join_theory);
Thu, Jul 16, 10:55 PM
florian.haftmann committed rISABELLEb8bcdb884651: tuned grouping.
tuned grouping
Thu, Jul 16, 11:50 AM
florian.haftmann committed rISABELLE587d4681240c: yet another alias.
yet another alias
Thu, Jul 16, 11:50 AM

Wed, Jul 15

makarius committed rISABELLE7b112eedc859: more robust wrt. experimental changes in Poly/ML;.
more robust wrt. experimental changes in Poly/ML;
Wed, Jul 15, 8:33 PM
makarius committed rISABELLEbc85d93aad23: more robust: handle unavailable statistics;.
more robust: handle unavailable statistics;
Wed, Jul 15, 7:48 PM
makarius committed rISABELLEc6756adfef0f: merged.
merged
Wed, Jul 15, 5:07 PM
makarius committed rISABELLE254c324f31fd: clarified user counters: expose tasks to external monitor;.
clarified user counters: expose tasks to external monitor;
Wed, Jul 15, 5:07 PM
makarius committed rISABELLEaa6a36c730c9: proper platform path for Windows;.
proper platform path for Windows;
Wed, Jul 15, 5:07 PM
makarius committed rISABELLEe48a5b6b7554: clarified signature;.
clarified signature;
Wed, Jul 15, 5:07 PM
makarius committed rISABELLE25d5ef16401a: support for monitoring of external ML process;.
support for monitoring of external ML process;
Wed, Jul 15, 5:07 PM
makarius committed rISABELLE452073b64f28: clarified signature;.
clarified signature;
Wed, Jul 15, 5:07 PM
makarius committed rISABELLE70bfda10f597: more robust;.
more robust;
Wed, Jul 15, 5:07 PM
makarius committed rISABELLEa25c7c686176: support for monitoring of external ML process;.
support for monitoring of external ML process;
Wed, Jul 15, 5:07 PM
makarius committed rISABELLEb7cec26e41d1: clarified modules: ML_Statistics within bootstrap environment;.
clarified modules: ML_Statistics within bootstrap environment;
Wed, Jul 15, 5:07 PM
makarius committed rISABELLEeece87547736: misc tuning and modernization;.
misc tuning and modernization;
Wed, Jul 15, 5:07 PM
makarius committed rISABELLE83456d9f0ed5: clarified examples;.
clarified examples;
Wed, Jul 15, 5:07 PM

Tue, Jul 14

dcjm committed rPOLYML94c8208a89c8: Add a related check for offsets that could exceed a signed 32-bit value. (authored by dcjm).
Add a related check for offsets that could exceed a signed 32-bit value.
Tue, Jul 14, 9:18 AM
dcjm committed rPOLYML0d77169373c6: Short constant index values can be put into the offset but leave larger and… (authored by dcjm).
Short constant index values can be put into the offset but leave larger and…
Tue, Jul 14, 9:18 AM
dcjm committed rPOLYMLc66cec192bdd: Modify test so that it works if int is IntInf.int. (authored by dcjm).
Modify test so that it works if int is IntInf.int.
Tue, Jul 14, 9:18 AM
kleing committed rAFP8c7430699dc1: merge from afp-2020.
merge from afp-2020
Tue, Jul 14, 4:40 AM
kleing committed rAFPc645808bafa7: update maintenance docs.
update maintenance docs
Tue, Jul 14, 4:40 AM

Mon, Jul 13

florian.haftmann committed rISABELLE08f1e4cb735f: concatentation of bit values.
concatentation of bit values
Mon, Jul 13, 7:25 PM
florian.haftmann committed rAFPce2c72a0a05e: concatentation of bit values.
concatentation of bit values
Mon, Jul 13, 7:23 PM
Sophie Tourret <stourret@mpi-inf.mpg.de> committed rAFPc99668f88e5f: saturation framework: renamings.
saturation framework: renamings
Mon, Jul 13, 2:51 PM
florian.haftmann committed rISABELLE759532ef0885: prefer canonically oriented lists of bits and more direct characterizations in….
prefer canonically oriented lists of bits and more direct characterizations in…
Mon, Jul 13, 8:08 AM