Page MenuHomeIsabelle/Phabricator

proversProject
ActivePublic

Details

Description

External provers for Sledgehammer, SMT etc.

Recent Activity

Mar 17 2021

mathias.fleury added a comment to T29: Update component for Z3.

Basically currently the proof format of Z3 has bugs that we cannot solve on the Isabelle side (https://github.com/Z3Prover/z3/issues/5073). Fixing those requires either internal Z3 knowledge or time from a Z3 developer.

Mar 17 2021, 6:28 PM · provers

Jan 7 2021

makarius moved T34: Update component for Vampire from TODO to Backlog on the isabelle-release board.
Jan 7 2021, 1:51 PM · provers, isabelle-release
makarius renamed T24: Missing minisat.dll for nitpick/kodkod on Windows (and Apple Silicon) from Missing minisat.dll for nitpick/kodkod on Windows to Missing minisat.dll for nitpick/kodkod on Windows (and Apple Silicon).
Jan 7 2021, 1:37 PM · provers, isabelle-release
makarius added a comment to T24: Missing minisat.dll for nitpick/kodkod on Windows (and Apple Silicon).

Also missing: arm64-linux, arm64-darwin (relavant for native JDK on macOS).

Jan 7 2021, 1:18 PM · provers, isabelle-release
makarius closed T30: Component and Isabelle/ML setup for Zipperposition as Resolved.

See Isabelle/162b71f7e554 and Isabelle/11de287ed481.

Jan 7 2021, 1:17 PM · provers

Dec 18 2020

makarius moved T30: Component and Isabelle/ML setup for Zipperposition from Backlog to TODO on the provers board.
Dec 18 2020, 12:16 PM · provers
makarius moved T34: Update component for Vampire from Backlog to TODO on the provers board.
Dec 18 2020, 12:16 PM · provers, isabelle-release
makarius moved T34: Update component for Vampire from Backlog to TODO on the isabelle-release board.
Dec 18 2020, 11:54 AM · provers, isabelle-release
makarius moved T34: Update component for Vampire from TODO to Backlog on the isabelle-release board.
Dec 18 2020, 11:51 AM · provers, isabelle-release
makarius moved T24: Missing minisat.dll for nitpick/kodkod on Windows (and Apple Silicon) from TODO to Backlog on the isabelle-release board.
Dec 18 2020, 11:51 AM · provers, isabelle-release
makarius moved T34: Update component for Vampire from Backlog to TODO on the isabelle-release board.
Dec 18 2020, 11:51 AM · provers, isabelle-release
makarius moved T24: Missing minisat.dll for nitpick/kodkod on Windows (and Apple Silicon) from Backlog to TODO on the isabelle-release board.
Dec 18 2020, 11:51 AM · provers, isabelle-release
makarius added a member for provers: blanchette.
Dec 18 2020, 11:21 AM
makarius added a member for provers: mathias.fleury.
Dec 18 2020, 11:21 AM
makarius added members for provers: makarius, martin.desharnais.
Dec 18 2020, 11:20 AM
makarius added a comment to T30: Component and Isabelle/ML setup for Zipperposition.

Isabelle/4a652d3f4522 provides isabelle build_zipperposition for 2.0 from OPAM. It works uniformly for Linux, macOS, Windows/Cygwin.

Dec 18 2020, 11:18 AM · provers

Dec 13 2020

makarius added a comment to T34: Update component for Vampire.

Isabelle/6751057a64b1 provides isabelle build_vampire for two versions: regular (stable) vampire, and experimental (latest) vampire_polymorphic. The latter does not build on Windows/Cygwin, though:

scope
  489 |         case DT_REG:
      |              ^~~~~~
/tmp/isabelle-wenzelm/build3185647966287583615/vampire/Lib/System.cpp:492:14:
error: ÔÇÿDT_DIRÔÇÖ was not declared in this scope
  492 |         case DT_DIR:
      |              ^~~~~~
make[2]: *** [CMakeFiles/obj.dir/build.make:304:
CMakeFiles/obj.dir/Lib/System.cpp.o] Error 1
make[2]: *** Waiting for unfinished jobs....
/tmp/isabelle-wenzelm/build3185647966287583615/vampire/Lib/Timer.cpp: In
static member function ÔÇÿstatic void Lib::Timer::suspendTimerBeforeFork()ÔÇÖ:
/tmp/isabelle-wenzelm/build3185647966287583615/vampire/Lib/Timer.cpp:155:11:
error: ÔÇÿsetitimerÔÇÖ was not declared in this scope
  155 |   int res=setitimer(ITIMER_REAL, &tv1, &tv2);
      |           ^~~~~~~~~
Dec 13 2020, 12:55 PM · provers, isabelle-release

Dec 4 2020

makarius claimed T34: Update component for Vampire.
Dec 4 2020, 12:43 PM · provers, isabelle-release
makarius triaged T34: Update component for Vampire as Normal priority.
Dec 4 2020, 12:43 PM · provers, isabelle-release

Nov 22 2020

makarius closed T28: Update component for CVC4 as Resolved.

Isabelle/dcc0022f0179 provides a manually assembled component, without isabelle build_cvc4 tool.

Nov 22 2020, 1:45 PM · provers, isabelle-release

Oct 31 2020

mathias.fleury closed T25: Update component for veriT as Resolved.

The veriT version is sufficient for the next release.

Oct 31 2020, 7:18 AM · provers, isabelle-release

Oct 29 2020

makarius triaged T26: Update component for E prover as Normal priority.
Oct 29 2020, 5:52 PM · provers, isabelle-release
makarius added a project to T20: Sledgehammer/z3: "bad SMT term: _": provers.
Oct 29 2020, 5:20 PM · provers
makarius added a project to T24: Missing minisat.dll for nitpick/kodkod on Windows (and Apple Silicon): provers.
Oct 29 2020, 5:19 PM · provers, isabelle-release
makarius added a project to T25: Update component for veriT: provers.
Oct 29 2020, 5:18 PM · provers, isabelle-release
makarius added a project to T27: Update component for SPASS: provers.
Oct 29 2020, 5:18 PM · provers, isabelle-release
makarius added a project to T28: Update component for CVC4: provers.
Oct 29 2020, 5:18 PM · provers, isabelle-release
makarius added a project to T29: Update component for Z3: provers.
Oct 29 2020, 5:17 PM · provers
makarius added a project to T30: Component and Isabelle/ML setup for Zipperposition: provers.
Oct 29 2020, 5:17 PM · provers
makarius added a project to T26: Update component for E prover: provers.
Oct 29 2020, 5:17 PM · provers, isabelle-release
makarius renamed provers from prover to provers.
Oct 29 2020, 5:16 PM
makarius created provers.
Oct 29 2020, 5:15 PM