# HG changeset patch
# User wenzelm
# Date 1714587178 -7200
# Node ID dff9cf737a53c6e163a817c1cab0fbea33f718f2
# Parent  8491d5fc0d57109b83d83618e05b80ed5c46ed63
build e-3.1, without patch;

diff -r 8491d5fc0d57 -r dff9cf737a53 src/Pure/Admin/component_e.scala
--- a/src/Pure/Admin/component_e.scala	Wed May 01 20:11:36 2024 +0200
+++ b/src/Pure/Admin/component_e.scala	Wed May 01 20:12:58 2024 +0200
@@ -10,7 +10,7 @@
 object Component_E {
   /* build E prover */
 
-  val default_version = "3.0.03"
+  val default_version = "3.1"
   val default_download_url = "https://wwwlehre.dhbw-stuttgart.de/~sschulz/WORK/E_DOWNLOAD"
 
   def build_e(
@@ -45,48 +45,6 @@
       Isabelle_System.extract(archive_path, component_dir.src, strip = true)
 
 
-      /* patch */
-
-      // proper support for trivial statements, e.g.
-      // fof(m__,conjecture,(! [X] : (p(X) => p(X)))).
-      val patch = """diff -ru E/CLAUSES/ccl_tcnf.c E-patched/CLAUSES/ccl_tcnf.c
---- E/CLAUSES/ccl_tcnf.c	2023-11-25 08:34:08.000000000 +0100
-+++ E-patched/CLAUSES/ccl_tcnf.c	2024-04-24 16:42:13.948892558 +0200
-@@ -254,14 +254,14 @@
-          }
-          else if(TermIsTrueTerm(form->args[0]))
-          {
--            handle = TFormulaFCodeAlloc(terms, terms->sig->eqn_code,
-+            handle = TFormulaFCodeAlloc(terms, terms->sig->neqn_code,
-                                         form->args[0],
-                                         form->args[0]);
- 
-          }
-          else if(TermIsFalseTerm(form->args[0]))
-          {
--            handle = TFormulaFCodeAlloc(terms, terms->sig->neqn_code,
-+            handle = TFormulaFCodeAlloc(terms, terms->sig->eqn_code,
-                                         form->args[0],
-                                         form->args[0]);
- 
-diff -ru E/CLAUSES/ccl_tformulae.c E-patched/CLAUSES/ccl_tformulae.c
---- E/CLAUSES/ccl_tformulae.c	2023-11-25 08:34:08.000000000 +0100
-+++ E-patched/CLAUSES/ccl_tformulae.c	2024-04-24 16:26:31.351672232 +0200
-@@ -2444,6 +2444,7 @@
-          else if(TermIsTrueTerm(form))
-          {
-             lit = EqnAlloc(form, form, terms, true);
-+            PStackPushP(lit_stack, lit);
-          }
-          else if(TermIsFalseTerm(form))
-          {
-"""
-
-      for (dir <- List(source_dir, component_dir.src)) {
-        Isabelle_System.bash("patch -b -p1", input = patch, cwd = dir.file).check
-      }
-
-
       /* build */
 
       progress.echo("Building E prover for " + platform_name + " ...")
@@ -128,10 +86,6 @@
       File.write(component_dir.README,
         "This is E prover " + version + " from\n" + archive_url + """
 
-* The sources have been patched as follows:
-
-""" + patch + """
-
 * The distribution has been built like this:
 
     cd src && """ + build_script + """