Page MenuHomeIsabelle/Phabricator

Update component for Vampire
Closed, ResolvedPublic

Description

Provide isabelle build_vampire and follow a suitable version from the repository
https://github.com/vprover/vampire

Event Timeline

makarius triaged this task as Normal priority.
makarius created this task.

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);
      |           ^~~~~~~~~
makarius moved this task from TODO to Backlog on the isabelle-release board.