Skip to content
[Jenkins]Jenkins
log in
Success

Changes

Changes from Mercurial (hg https://isabelle.in.tum.de/repos/isabelle/ default)

Summary

  1. provide cvc5-1.1.1 for testing --- still inactive;
  2. rebuild bash_process executables on current reference platforms, including native arm64-darwin; enforce rebuild of Isabelle/Scala + Isabelle/ML;
  3. tuned NEWS, see also c62003e05e46;
  4. update NEWS, following ea1913c953ef;
  5. tuned whitespace according to jEdit mode parameters ":wrap=hard:maxLineLen=72:";
  6. more explicit NEWS (see 3648e9c88d0c);
  7. NEWS for a53287d9add3, 3e30ca77ccfe;
  8. add option for unify trace (now disabled by default as printing is excessive and rarely used);
  9. tuned unify trace option names;
Changeset 79750:f8fb4384180e by wenzelm:
provide cvc5-1.1.1 for testing --- still inactive;
The file was modified Admin/components/components.sha1
The file was modified src/Pure/Admin/component_cvc5.scala
Changeset 79749:a861b0df74b4 by wenzelm:
rebuild bash_process executables on current reference platforms, including native arm64-darwin;<br>enforce rebuild of Isabelle/Scala + Isabelle/ML;
The file was modified Admin/bash_process/build
The file was modified Admin/bash_process/etc/settings
The file was modified Admin/components/components.sha1
The file was modified Admin/components/main
The file was modified src/Pure/ROOT.ML
The file was modified src/Pure/ROOT.scala
Changeset 79748:e84b480e90e4 by wenzelm:
tuned NEWS, see also c62003e05e46;
The file was modified NEWS
Changeset 79747:023b34159050 by wenzelm:
update NEWS, following ea1913c953ef;
The file was modified NEWS
Changeset 79746:71dce74a456e by wenzelm:
tuned whitespace according to jEdit mode parameters &quot;:wrap=hard:maxLineLen=72:&quot;;
The file was modified NEWS
Changeset 79745:779cfa2573da by wenzelm:
more explicit NEWS (see 3648e9c88d0c);
The file was modified NEWS
Changeset 79744:1cbae8af034c by wenzelm:
NEWS for a53287d9add3, 3e30ca77ccfe;
The file was modified NEWS
Changeset 79743:3648e9c88d0c by fabian huch _huch@in.tum.de_:
add option for unify trace (now disabled by default as printing is excessive and rarely used);
The file was modified NEWS
The file was modified src/Doc/Isar_Ref/Generic.thy
The file was modified src/Doc/Logics/document/HOL.tex
The file was modified src/HOL/Tools/try0.ML
The file was modified src/Pure/Isar/attrib.ML
The file was modified src/Pure/unify.ML
Changeset 79742:2e4518e8a36b by fabian huch _huch@in.tum.de_:
tuned unify trace option names;
The file was modified src/Doc/Logics/document/HOL.tex
The file was modified src/HOL/Tools/try0.ML
The file was modified src/Pure/Isar/attrib.ML
The file was modified src/Pure/unify.ML

Changes from Mercurial (hg https://foss.heptapod.net/isa-afp/afp-devel/ default)

Summary

  1. backed out changeset ddf90847bfa5: still requires approx. 8-10h elapsed time / 50h CPU time on common test hardware (see 13b3e24a71b0), only latest x86_64-linux hardware is reasonably fast (3.5h elapsed time, 20h CPU time seen on of1.proof.cit.tum.de), but arm64-darwin is very slow;
  2. tuned signature, following Isabelle/da4e82434985;
  3. adapted to Isabelle/3648e9c88d0c;
Changeset 14080:fd41e17fc7bd by wenzelm:
backed out changeset ddf90847bfa5: still requires approx. 8-10h elapsed time / 50h CPU time on common test hardware (see 13b3e24a71b0), only latest x86_64-linux hardware is reasonably fast (3.5h elapsed time, 20h CPU time seen on of1.proof.cit.tum.de), but arm64-darwin is very slow;
The file was modified thys/Ordinary_Differential_Equations/Ex/Lorenz/C1/Lorenz_C1.thy
The file was modified thys/Ordinary_Differential_Equations/ROOT
Changeset 14079:38e4f6bce76e by wenzelm:
tuned signature, following Isabelle/da4e82434985;
The file was modified tools/web_app.scala
Changeset 14078:3fdc5d919d7c by fabian huch _huch@in.tum.de_:
adapted to Isabelle/3648e9c88d0c;
The file was modified thys/ML_Unification/ML_Utils/Tactics/tactic_util.ML