# HG changeset patch
# User wenzelm
# Date 1713980925 -7200
# Node ID 8e3730b527e98e22c52bcbeda6a7a3f0a1c23f78
# Parent  e9ea4d88490d8f35f73ed335685bdc8d279c3b7f
minor patch for E Prover, based on "git diff -w -r E-3.0.03 E-3.0.08": proper support for trivial statements;

diff -r e9ea4d88490d -r 8e3730b527e9 src/Pure/Admin/component_e.scala
--- a/src/Pure/Admin/component_e.scala	Sat Apr 20 17:10:34 2024 +0200
+++ b/src/Pure/Admin/component_e.scala	Wed Apr 24 19:48:45 2024 +0200
@@ -43,6 +43,48 @@
       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 + " ...")
@@ -84,11 +126,15 @@
       File.write(component_dir.README,
         "This is E prover " + version + " from\n" + archive_url + """
 
-The distribution has been built like this:
+* The sources have been patched as follows:
+
+""" + patch + """
+
+* The distribution has been built like this:
 
     cd src && """ + build_script + """
 
-Only a few executables from PROVERS/ have been moved to the platform-specific
+* Some executables from PROVERS/ have been moved to the platform-specific
 Isabelle component directory: x86_64-linux etc.