Fix ubuntu CI failiures

linux/snap/snapcraft.yaml.in

@@ -11,7 +11,8 @@ confinement: strict
 parts:
   coq:
     plugin: nil
-    build-packages: [build-essential, curl, m4, unzip, git, libstdc++-7-dev]
+    # Note: to find out which libstdc++ version is required, enter a shell with "multipass shell snapcraft-coq-prover" and run "gcc-version" there.
+    build-packages: [build-essential, curl, m4, unzip, git, libstdc++-9-dev]
     stage-packages: [make, libmpfr6, libgmp10]
     source: .
     source-type: local

opam/opam-coq-archive/released/packages/coq-gappa-flocq3/coq-gappa-flocq3.1.5.1/opam

@@ -8,7 +8,7 @@ patches: [
   "0001-Rename-Flocq-to-Flocq3.patch"
 ]
 build: [
-  ["autoconf"]
+  ["autoreconf" "-f"]
   ["./configure"]
   ["./remake" "-j%{jobs}%"]
 ]

opam/opam-coq-archive/released/packages/coq-metacoq-template/coq-metacoq-template.1.1+8.15/opam

@@ -20,11 +20,9 @@ authors: ["Abhishek Anand <aa755@cs.cornell.edu>"
 license: "MIT"
 patches: [
   "0001-Fix-line-ending-issues-with-generated-code-on-Window.patch"
-  "Fix make issues Coq Platform CI.patch"
 ]
 build: [
   ["bash" "./configure.sh"]
-  ["rm" "-f" "template-coq/_PluginProject" "template-coq/_TemplateCoqProject"]
   [make "-j" "%{jobs}%" "template-coq"]
 ]
 install: [

opam/opam-coq-archive/released/packages/coq-metacoq-template/coq-metacoq-template.1.1+8.16/opam

@@ -20,11 +20,9 @@ authors: ["Abhishek Anand <aa755@cs.cornell.edu>"
 license: "MIT"
 patches: [
   "0001-Fix-line-ending-issues-with-generated-code-on-Window.patch"
-  "Fix make issues Coq Platform CI.patch"
 ]
 build: [
   ["bash" "./configure.sh"]
-  ["rm" "-f" "template-coq/_PluginProject" "template-coq/_TemplateCoqProject"]
   [make "-j" "%{jobs}%" "template-coq"]
 ]
 install: [

opam/opam-coq-archive/released/packages/coq-metacoq-template/coq-metacoq-template.1.2+8.16/opam

@@ -22,7 +22,6 @@ license: "MIT"
 patches: [ "Fix make issues Coq Platform CI.patch" ]
 build: [
   ["bash" "./configure.sh"]
-  ["rm" "-f" "template-coq/_PluginProject" "template-coq/_TemplateCoqProject"]
   [make "-j" "%{jobs}%" "template-coq"]
 ]
 install: [

opam/opam-coq-archive/released/packages/coq-metacoq-template/coq-metacoq-template.1.2+8.17/opam

@@ -22,7 +22,6 @@ license: "MIT"
 patches: [ "Fix make issues Coq Platform CI.patch" ]
 build: [
   ["bash" "./configure.sh"]
-  ["rm" "-f" "template-coq/_PluginProject" "template-coq/_TemplateCoqProject"]
   [make "-j" "%{jobs}%" "template-coq"]
 ]
 install: [

opam/opam-coq-archive/released/packages/coq-metacoq-template/coq-metacoq-template.1.2.1+8.18/opam

@@ -22,7 +22,6 @@ license: "MIT"
 patches: [ "Fix make issues Coq Platform CI.patch" ]
 build: [
   ["bash" "./configure.sh"]
-  ["rm" "-f" "template-coq/_PluginProject" "template-coq/_TemplateCoqProject"]
   [make "-j" "%{jobs}%" "-C" "template-coq"]
 ]
 install: [

opam/opam-coq-archive/released/packages/coq-metacoq-template/coq-metacoq-template.1.3.1+8.19/opam

@@ -22,7 +22,6 @@ license: "MIT"
 patches: [ "Fix make issues Coq Platform CI.patch" ]
 build: [
   ["bash" "./configure.sh"]
-  ["rm" "-f" "template-coq/_PluginProject" "template-coq/_TemplateCoqProject"]
   [make "-j" "%{jobs}%" "-C" "template-coq"]
 ]
 install: [

opam/opam-repository/packages/gappa/gappa.1.3.5/opam

@@ -0,0 +1,61 @@
+opam-version: "2.0"
+maintainer: "7895506+MSoegtropIMC@users.noreply.github.com"
+authors: "Guillaume Melquiond"
+bug-reports: "https://gitlab.inria.fr/gappa/gappa/-/issues"
+homepage: "https://gitlab.inria.fr/gappa/gappa"
+dev-repo: "git+https://gitlab.inria.fr/gappa/gappa.git"
+license: "CeCILL"
+patches: [
+  "remake.patch"
+  "0001-Added-configure-for-c-11.patch"
+]
+build: [
+  [ "autoreconf" ]
+  # Note: configure.in seems to reference this file
+  [ "touch" "stamp-config_h.in" ]
+  [ "./configure"
+    # If someone knows how to ask MacPorts for the usual include and lib path, please tell me
+    "CXXFLAGS=-I/opt/local/include" { os-distribution = "macports" & os = "macos" }
+    "LDFLAGS=-L/opt/local/lib" { os-distribution = "macports" & os = "macos" }
+    # Support installing on Apple Silicon with Homebrew
+    "CXXFLAGS=-I/opt/homebrew/include" { os-distribution = "homebrew" & os = "macos" & arch = "arm64"}
+    "LDFLAGS=-L/opt/homebrew/lib" { os-distribution = "homebrew" & os = "macos" & arch = "arm64"}
+    "--build=%{arch}%-pc-cygwin" { os = "win32" & os-distribution = "cygwinports" }
+    "--host=%{arch}%-w64-mingw32" { os = "win32" & os-distribution = "cygwinports" }
+    "--target=%{arch}%-w64-mingw32" { os = "win32" & os-distribution = "cygwinports" }
+    "--prefix=%{prefix}%" 
+  ]
+  [ "./remake" "--jobs=%{jobs}%" ]
+]
+install: [ "./remake" "-d" "install" ]
+depends: [
+  "conf-g++" {build}
+  "conf-autoconf" {build}
+  "conf-automake" {build}
+  "conf-gmp"
+  "conf-mpfr"
+  "conf-boost"
+  "conf-bison" {build}
+  "conf-flex" {build}
+]
+synopsis: "Tool intended for formally proving properties on numerical programs dealing with floating-point or fixed-point arithmetic"
+url {
+  src: "https://gappa.gitlabpages.inria.fr/releases/gappa-1.3.5.tar.gz"
+  checksum: "sha512=60b5719e3a321df43e33045fa8f4511fc02a4218d1ae7e476e7c6ebcf90ae208832881f6eea5b99a3296dfcc3a18c7e1f4ea9dbea446fc502e14306b6975f6e6"
+}
+extra-source "remake.patch" {
+  src:
+    "https://raw.githubusercontent.com/ocaml/opam-source-archives/main/patches/gappa/remake.patch"
+  checksum: [
+    "sha256=365967b9cd294d485302b6c14a072ac06d3238bfeb313eaae07159a8542fc5ff"
+    "md5=d66b718118ae5bf61c661905f6f0db96"
+  ]
+}
+extra-source "0001-Added-configure-for-c-11.patch" {
+  src:
+    "https://raw.githubusercontent.com/ocaml/opam-source-archives/main/patches/gappa/0001-Added-configure-for-c-11.patch"
+  checksum: [
+    "sha256=5d9ff1e6461834c2d3d6c4cb1f9dd7424a4a681b40cab19a6fbbe0ff8d50284e"
+    "md5=b6a6dbe9a12feae79eab038864208a3c"
+  ]
+}

package_picks/package-pick-8.15~2022.04.sh

@@ -122,8 +122,8 @@ then
   PACKAGES="${PACKAGES} coq-aac-tactics.8.15.1"
   PACKAGES="${PACKAGES} coq-unicoq.1.6+8.15"
   PACKAGES="${PACKAGES} coq-mtac2.1.4+8.15"
-  PACKAGES="${PACKAGES} coq-elpi.1.13.0 elpi.1.14.3"
-  PACKAGES="${PACKAGES} coq-hierarchy-builder.1.2.1"
+  PACKAGES="${PACKAGES} elpi.1.15.2 coq-elpi.1.14.0" #The previous used version was broken, so we use the same as the next 8.15 pick
+  PACKAGES="${PACKAGES} coq-hierarchy-builder.1.3.0" #Had to additionally upgrade hierarchy builder due to dependency constraints
   PACKAGES="${PACKAGES} coq-quickchick.1.6.1"
   PACKAGES="${PACKAGES} coq-hammer-tactics.1.3.2+8.15"
   if [[ "$OSTYPE" != cygwin ]]
@@ -138,7 +138,7 @@ then
   PACKAGES="${PACKAGES} coq-libhyps.2.0.5"
 
   # General mathematics (which requires one of the above tools)
-  PACKAGES="${PACKAGES} coq-mathcomp-analysis.0.5.0"
+  PACKAGES="${PACKAGES} coq-mathcomp-analysis.0.5.4"
   PACKAGES="${PACKAGES} coq-relation-algebra.1.7.7"
 
   # Formal languages, compilers and code verification

shell_scripts/build.sh

@@ -45,7 +45,7 @@ case "$COQ_PLATFORM_PARALLEL" in
         echo PINNING $package
         package_name="$(echo "$package" | cut -d '.' -f 2)"
         package_version="$(echo "$package" | cut -d '.' -f 3-)"
-        if ! $COQ_PLATFORM_TIME opam pin ${package_name} ${package_version}; then dump_opam_logs; fi
+        if ! $COQ_PLATFORM_TIME opam pin --no-action ${package_name} ${package_version}; then dump_opam_logs; fi
         ;;
       esac
     done