Page MenuHomeIsabelle/Phabricator

Update component for E prover
Closed, ResolvedPublic

Description

Routine update of "e" for sledgehammer: jump from old 2.0 to current 2.5.

Event Timeline

makarius claimed this task.

Isabelle/cd3419427cd3 already has E prover 2.5 for production use.

There was a minor build problem on Windows/Cygwin64 (version 3.1.7-1 from 24-Aug-2020):

../lib/TERMS.a(cte_termbanks.o):cte_termbanks.c:(.rdata$.refptr.TFormulaTSTPParse[.refptr.TFormulaTSTPParse]+0x0):
undefined reference to `TFormulaTSTPParse'
collect2: error: ld returned 1 exit status
make[1]: *** [Makefile:41: term2dag] Error 1
make[1]: Leaving directory '/home/wenzelm/isabelle/repos/e-2.5/src/SIMPLE_APPS'

According to Stephan Schulz (03-Oct-2020) this can be ignored for now: it works for us in Isabelle2021.

makarius triaged this task as Normal priority.Oct 29 2020, 5:52 PM