feat: Update build system with mathcomp >= 2.0 and coqeal dev, before…

… it is released href: coq-community/coqeal#87 Co-authored-by: Pierre Roux <[email protected]>
validsdp · Feb 2, 2024 · d85f1ad · d85f1ad
1 parent 4a102fc
commit d85f1ad
Show file tree

Hide file tree

Showing 8 changed files with 34 additions and 1,024 deletions.
diff --git a/.github/workflows/coq-action.yml b/.github/workflows/coq-action.yml
@@ -15,13 +15,11 @@ jobs:
     strategy:
       matrix:
         image:
-          - mathcomp/mathcomp:1.18.0-coq-8.18
-          - mathcomp/mathcomp:1.18.0-coq-8.17
-          - mathcomp/mathcomp:1.18.0-coq-8.16
-          - mathcomp/mathcomp:1.17.0-coq-8.17
-          - mathcomp/mathcomp:1.17.0-coq-8.15
-          - mathcomp/mathcomp:1.16.0-coq-8.15
-          - mathcomp/mathcomp:1.15.0-coq-8.15
+          # - mathcomp/mathcomp:2.2.0-coq-8.19
+          - mathcomp/mathcomp:2.2.0-coq-8.18
+          - mathcomp/mathcomp:2.2.0-coq-8.17
+          - mathcomp/mathcomp:2.1.0-coq-8.17          
+          - mathcomp/mathcomp:2.0.0-coq-8.16
       fail-fast: false
     steps:
     - uses: actions/checkout@v2

diff --git a/Makefile.in b/Makefile.in
@@ -34,17 +34,7 @@ $(PLUGDIR)/src/soswitness.mlg: $(PLUGDIR)/src/soswitness_@[email protected]
 	chmod a-w $@
 
 $(COQ_MAKEFILE): $(COQ_PROJ) $(MODULES) $(PLUGDIR)/src/soswitness.mlg
-	if [ "x@ADD_INCLUDES@" = "xyes" ] ; then \
-	  ocamlfind query zarith >/dev/null ; \
-	  ocamlfind query ocplib-simplex >/dev/null ; \
-	  ocamlfind query osdp >/dev/null ; \
-	  $(COQBIN)coq_makefile \
-	    -I "$(shell ocamlfind query zarith)" \
-	    -I "$(shell ocamlfind query ocplib-simplex)" \
-	    -I "$(shell ocamlfind query osdp)" \
-	    @LTAC2_CAML_FILES@ \
-	    -f $< $(MODULES) -o $@ ; \
-	else $(COQBIN)coq_makefile -f $< $(MODULES) -o $@ ; fi
+	$(COQBIN)coq_makefile -f $< $(MODULES) -o $@
 	# FIXME: This sed hack is fragile (if we do "make -B" for example)
 	sed -e 's/-shared -o $$@ $$</-shared -o $$@ ocplibSimplex.cmxa osdp.cmxa $$</' -i $@
 

diff --git a/configure.ac b/configure.ac
@@ -17,8 +17,8 @@ AS_IF([test "x$COQC" = xno], [AC_MSG_ERROR([Cannot find coqc.])])
 AC_MSG_CHECKING(Coq version)
 coq_version=`$COQC -v | grep version | sed -e 's/^.*version \([[0-9.+a-z]]*\).*$/\1/'`
 AC_MSG_RESULT($coq_version)
-AX_VERSION_GE([$coq_version], 8.14, [],
-  [ AC_MSG_ERROR([must be at least 8.14.]) ])
+AX_VERSION_GE([$coq_version], 8.16, [],
+  [ AC_MSG_ERROR([must be at least 8.16.]) ])
 AC_CHECK_TOOL([OCAMLFIND], [ocamlfind], [no])
 AS_IF([test "x$OCAMLFIND" = xno], [AC_MSG_ERROR([Cannot find ocamlfind.])])
 
@@ -27,26 +27,20 @@ AC_MSG_CHECKING([for Ltac2])
 COQTOP_WHERE=`coqtop -where`
 LTAC2_DIR="${COQTOP_WHERE}-core/plugins/ltac2"
 AS_IF([test -d ${LTAC2_DIR}],
-  [ LTAC2_CAML_FILES="${LTAC2_CAML_FILES} -I ${LTAC2_DIR}"
-    AC_MSG_RESULT([yes]) ],
+  [ AC_MSG_RESULT([yes]) ],
   [ AC_MSG_RESULT([no])
-    AC_MSG_ERROR([ *** Unable to find Ltac2 which should be installed with Coq >= 8.12])])
-AC_SUBST(LTAC2_CAML_FILES)
-COQ_VERSION="v814"
+    AC_MSG_ERROR([ *** Unable to find Ltac2 which should be installed with Coq])])
+COQ_VERSION="v816"
 SOSWIT_PLUGIN_EXT="soswitness"
-AX_VERSION_GE([$coq_version], 8.15, [COQ_VERSION="v815"], [])
-AX_VERSION_GE([$coq_version], 8.16,
-  [COQ_VERSION="v816"; ADD_INCLUDES="no"; SOSWIT_PLUGIN="soswitness:coq-validsdp.plugin";
-   META_FILE="plugins/soswitness/src/META.coq-validsdp";
-   CAMLPKGS="-package coq-core.plugins.ltac2 \
-    -package zarith \
-    -package ocplib-simplex \
-    -package osdp"],
-  [ADD_INCLUDES="yes"; SOSWIT_PLUGIN="soswitness"; META_FILE=""; CAMLPKGS=""])
+SOSWIT_PLUGIN="soswitness:coq-validsdp.plugin"
+META_FILE="plugins/soswitness/src/META.coq-validsdp"
+CAMLPKGS="-package coq-core.plugins.ltac2 \
+  -package zarith \
+  -package ocplib-simplex \
+  -package osdp"
 AX_VERSION_GE([$coq_version], 8.18,
   [COQ_VERSION="v818"; SOSWIT_PLUGIN_EXT="coq-validsdp.plugin"], [])
 AC_SUBST(COQ_VERSION)
-AC_SUBST(ADD_INCLUDES)
 AC_SUBST(SOSWIT_PLUGIN)
 AC_SUBST(SOSWIT_PLUGIN_EXT)
 AC_SUBST(META_FILE)
@@ -58,7 +52,7 @@ AS_IF(
     $COQC conftest.v > conftest.err ],
   [ AC_MSG_RESULT([yes]) ],
   [ AC_MSG_RESULT([no])
-    AC_MSG_ERROR([ *** Unable to find theories rat, matrix, countalg from mathcomp >= 1.12.0 (http://coq.io/opam/coq-mathcomp-field.1.12.0.html)])])
+    AC_MSG_ERROR([ *** Unable to find theories rat, matrix, countalg from coq-mathcomp-field])])
 rm -f conftest.v conftest.vo conftest.err
 
 AC_MSG_CHECKING([for Mathcomp Analysis])
@@ -67,7 +61,7 @@ AS_IF(
     $COQC conftest.v > conftest.err ],
   [ AC_MSG_RESULT([yes]) ],
   [ AC_MSG_RESULT([no])
-    AC_MSG_ERROR([ *** Unable to find theory Rstruct from mathcomp anaysis (http://coq.io/opam/coq-mathcomp-analysis.0.3.5.html)])])
+    AC_MSG_ERROR([ *** Unable to find theory Rstruct from coq-mathcomp-analysis])])
 rm -f conftest.v conftest.vo conftest.err
 
 AC_MSG_CHECKING([for Flocq])
@@ -77,7 +71,7 @@ AS_IF(
     $COQC conftest.v > conftest.err ],
   [ AC_MSG_RESULT([yes]) ],
   [ AC_MSG_RESULT([no])
-    AC_MSG_ERROR([ *** Unable to find library Flocq >= 3.1 (http://flocq.gforge.inria.fr/)])])
+    AC_MSG_ERROR([ *** Unable to find library Flocq >= 3.3 (http://flocq.gforge.inria.fr/)])])
 rm -f conftest.v conftest.vo conftest.err
 
 AC_MSG_CHECKING([for Coq-interval])

diff --git a/coq-libvalidsdp.opam b/coq-libvalidsdp.opam
@@ -17,13 +17,13 @@ build: [
 ]
 install: [make "-C" "libvalidsdp" "install"]
 depends: [
-  "coq" {((>= "8.15" & < "8.19~") | (= "dev"))}
+  "coq" {((>= "8.16" & < "8.20~") | (= "dev"))}
   "coq-bignums"
   "coq-flocq" {>= "3.3.0"}
   "coq-coquelicot" {>= "3.0"}
   "coq-interval" {>= "4.0.0" & < "5~"}
-  "coq-mathcomp-field" {(>= "1.15" & < "1.19~") | (= "dev")}
-  "coq-mathcomp-analysis" {>= "0.3.5"}
+  "coq-mathcomp-field" {(>= "2.0" & < "2.3~") | (= "dev")}
+  "coq-mathcomp-analysis" {>= "1.0.0"}
   "ocamlfind" {build}
   "conf-autoconf" {build & dev}
 ]

diff --git a/coq-validsdp.opam b/coq-validsdp.opam
@@ -20,15 +20,15 @@ install: [make "install"]
 
 depends: [
   "ocaml"
-  "coq" {((>= "8.15" & < "8.19~") | (= "dev"))}
+  "coq" {((>= "8.16" & < "8.20~") | (= "dev"))}
   "coq-bignums"
   "coq-flocq" {>= "3.3.0"}
   "coq-interval" {>= "4.0.0" & < "5~"}
-  "coq-mathcomp-field" {(>= "1.15" & < "1.19~") | (= "dev")}
-  "coq-mathcomp-analysis" {>= "0.3.5"}
-  "coq-libvalidsdp" {= "dev"}
-  "coq-mathcomp-multinomials" {>= "1.6"}
-  "coq-coqeal" {>= "1.1.3"}
+  "coq-mathcomp-field" {(>= "2.0" & < "2.3~") | (= "dev")}
+  "coq-mathcomp-analysis" {>= "1.0.0"}
+  "coq-libvalidsdp" {= version}
+  "coq-mathcomp-multinomials" {>= "2.0"}
+  "coq-coqeal" {= "dev"} # to update
   "coq-paramcoq" {>= "1.1.0"}
   "osdp" {>= "1.0"}
   "ocamlfind" {build}

diff --git a/libvalidsdp/configure.ac b/libvalidsdp/configure.ac
@@ -17,8 +17,8 @@ AS_IF([test "x$COQC" = xno], [AC_MSG_ERROR([Cannot find coqc.])])
 AC_MSG_CHECKING(Coq version)
 coq_version=`$COQC -v | grep version | sed -e 's/^.*version \([[0-9.+a-z]]*\).*$/\1/'`
 AC_MSG_RESULT($coq_version)
-AX_VERSION_GE([$coq_version], 8.14, [],
-  [ AC_MSG_ERROR([must be at least 8.14.]) ])
+AX_VERSION_GE([$coq_version], 8.16, [],
+  [ AC_MSG_ERROR([must be at least 8.16.]) ])
 
 AC_CHECK_TOOL([OCAMLFIND], [ocamlfind], [no])
 AS_IF([test "x$OCAMLFIND" = xno], [AC_MSG_ERROR([Cannot find ocamlfind.])])
@@ -30,7 +30,7 @@ AS_IF(
     $COQC conftest.v > conftest.err ],
   [ AC_MSG_RESULT([yes]) ],
   [ AC_MSG_RESULT([no])
-    AC_MSG_ERROR([ *** Unable to find theories rat, matrix, countalg from mathcomp >= 1.12.0 (http://coq.io/opam/coq-mathcomp-field.1.12.0.html)])])
+    AC_MSG_ERROR([ *** Unable to find theories rat, matrix, countalg from coq-mathcomp-field])])
 rm -f conftest.v conftest.vo conftest.err
 
 AC_MSG_CHECKING([for Mathcomp Analysis])
@@ -39,7 +39,7 @@ AS_IF(
     $COQC conftest.v > conftest.err ],
   [ AC_MSG_RESULT([yes]) ],
   [ AC_MSG_RESULT([no])
-    AC_MSG_ERROR([ *** Unable to find theory Rstruct from mathcomp anaysis (http://coq.io/opam/coq-mathcomp-analysis.0.3.5.html)])])
+    AC_MSG_ERROR([ *** Unable to find theory Rstruct from coq-mathcomp-analysis])])
 rm -f conftest.v conftest.vo conftest.err
 
 AC_MSG_CHECKING([for Flocq])
@@ -49,7 +49,7 @@ AS_IF(
     $COQC conftest.v > conftest.err ],
   [ AC_MSG_RESULT([yes]) ],
   [ AC_MSG_RESULT([no])
-    AC_MSG_ERROR([ *** Unable to find library Flocq >= 3.1 (http://flocq.gforge.inria.fr/)])])
+    AC_MSG_ERROR([ *** Unable to find library Flocq >= 3.3 (http://flocq.gforge.inria.fr/)])])
 rm -f conftest.v conftest.vo conftest.err
 
 AC_MSG_CHECKING([for Coq-interval])