Skip to content
[Jenkins]Jenkins
log in
Success

Changes

Summary

  1. rebuild "verit" for arm64-linux for more robustness, e.g. relevant for theory "HOL-ex.BigO"; uniform baseline for "linux" and "linux_arm";
  2. proper os_name "linux" instead of "linux_arm" (amending a33a6e541cbb);
  3. proper bash syntax (amending 0631dfc0db07);
  4. tuned proof: avoid z3;
  5. tuned proof: avoid z3 to make it work on arm64-linux;
  6. tuned proofs --- avoid smt with external prover, which is somewhat unstable on arm64-linux;
  7. merged
  8. more robust check of ISABELLE_PLATFORM_FAMILY within settings environment, to support its reunification with Isabelle/Scala (see also a33a6e541cbb, f3a356c64193);
  9. strengthened class parity
Changeset 79563:76ad72736e9e by wenzelm:
rebuild &quot;verit&quot; for arm64-linux for more robustness, e.g. relevant for theory &quot;HOL-ex.BigO&quot;;<br>uniform baseline for &quot;linux&quot; and &quot;linux_arm&quot;;
The file was modified Admin/components/PLATFORMS (diff)
The file was modified Admin/components/components.sha1 (diff)
The file was modified Admin/components/main (diff)
Changeset 79562:ceaef5bae253 by wenzelm:
proper os_name &quot;linux&quot; instead of &quot;linux_arm&quot; (amending a33a6e541cbb);
The file was modified src/Pure/System/isabelle_platform.scala (diff)
Changeset 79561:4838fcbd019b by wenzelm:
proper bash syntax (amending 0631dfc0db07);
The file was modified lib/Tools/scala (diff)
Changeset 79560:5c2c8a60b77e by wenzelm:
tuned proof: avoid z3;
The file was modified src/HOL/Library/Float.thy (diff)
Changeset 79559:cd9ede8488af by wenzelm:
tuned proof: avoid z3 to make it work on arm64-linux;
The file was modified src/HOL/ex/BigO.thy (diff)
Changeset 79558:58e974ef0625 by wenzelm:
tuned proofs --- avoid smt with external prover, which is somewhat unstable on arm64-linux;
The file was modified src/HOL/ex/Unification.thy (diff)
Changeset 79557:9f031b8bc880 by wenzelm:
merged
Changeset 79556:0631dfc0db07 by wenzelm:
more robust check of ISABELLE_PLATFORM_FAMILY within settings environment, to support its reunification with Isabelle/Scala (see also a33a6e541cbb, f3a356c64193);
The file was modified etc/settings (diff)
The file was modified lib/Tools/scala (diff)
The file was modified lib/scripts/getfunctions (diff)
The file was modified lib/scripts/getsettings (diff)
The file was modified lib/scripts/java-gui-setup (diff)
The file was modified src/Pure/Admin/component_jdk.scala (diff)
The file was modified src/Pure/System/isabelle_platform.scala (diff)
The file was modified src/Tools/VSCode/src/component_vscodium.scala (diff)
Changeset 79555:8ef205d9fd22 by haftmann:
strengthened class parity
The file was modified src/HOL/Bit_Operations.thy (diff)
The file was modified src/HOL/Library/Word.thy (diff)
The file was modified src/HOL/Parity.thy (diff)