Merge pull request #463 from MSoegtropIMC/2025.01-prep-8

2025.01 prep 8

coq_platform_make.sh

@@ -76,6 +76,10 @@ source shell_scripts/install_system_prerequisites.sh
 
 source shell_scripts/build.sh
 
+###################### FINALIZE #####################
+
+source shell_scripts/post_system.sh
+
 ###################### CLOSING #####################
 
 source shell_scripts/closing_remarks.sh

opam/opam-coq-archive/released/packages/coq-coqprime-generator/coq-coqprime-generator.1.1.2/opam

@@ -0,0 +1,45 @@
+opam-version: "2.0"
+maintainer: "thery@sophia.inria.fr"
+homepage: "https://github.com/thery/coqprime"
+bug-reports: "https://github.com/thery/coqprime/issues"
+dev-repo: "git+https://github.com/thery/coqprime.git"
+license: "LGPL-2.1-only"
+authors: ["Laurent Théry"]
+
+build: [
+  # cd to a subfolder in opam is tricky, so just move gencertif to the root folder
+  [ "find" "gencertif" "-type" "f" "-exec" "mv" "{}" "." ";" ]
+  [ "autoreconf" "-i" "-s" ]
+  [ "./configure" "--prefix" prefix
+    # Optiosn for finding opam local gmp-ecm
+    "CPPFLAGS=-I%{prefix}%/include"
+    "LDFLAGS=-L%{lib}%"
+    # Options for homebrew on Intel silicon (overwriting the above)
+    "CPPFLAGS=-I%{prefix}%/include -I/opt/local/include" { os-distribution = "macports" & os = "macos" }
+    "LDFLAGS=-L%{lib}% -L/opt/local/lib" { os-distribution = "macports" & os = "macos" }
+    # Options for homebrew on Apple silicon (overwriting the above)
+    "CPPFLAGS=-I%{prefix}%/include -I/opt/homebrew/include" { os-distribution = "homebrew" & os = "macos" & arch = "arm64"}
+    "LDFLAGS=-L%{lib}% -L/opt/homebrew/lib" { os-distribution = "homebrew" & os = "macos" & arch = "arm64"}
+    # Options for Windows cygwin
+    "--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" }
+  ]
+  [ make "-j" "%{jobs}%" ]
+]
+install: [
+  [make "install"]
+]
+depends: [
+  "ocaml" {>= "4.14.2"}
+  "ocamlfind"
+  "zarith"
+  "num"
+  "conf-gmp"
+  "gmp-ecm"
+]
+synopsis: "Certificate generator for prime numbers in Coq"
+url {
+  src: "https://github.com/thery/coqprime/archive/v8.20.1.tar.gz"
+  checksum: "sha512=8281e395b919fff9244287a75b2ab3ade21fc989e22185c4eb788706cc6a099a4be3de4435bdf60e5da32824a500b642ad8f7b759f2c4ddf0359f2d438413e68"
+}

opam/opam-coq-archive/released/packages/coq-corn/coq-corn.8.20.0/opam

@@ -0,0 +1,98 @@
+opam-version: "2.0"
+maintainer: "b.a.w.spitters@gmail.com"
+
+homepage: "https://github.com/coq-community/corn"
+dev-repo: "git+https://github.com/coq-community/corn.git"
+bug-reports: "https://github.com/coq-community/corn/issues"
+license: "GPL-2.0"
+
+synopsis: "The Coq Constructive Repository at Nijmegen"
+description: """
+CoRN includes the following parts:
+
+- Algebraic Hierarchy
+
+  An axiomatic formalization of the most common algebraic
+  structures, including setoids, monoids, groups, rings,
+  fields, ordered fields, rings of polynomials, real and
+  complex numbers
+
+- Model of the Real Numbers
+
+  Construction of a concrete real number structure
+  satisfying the previously defined axioms
+
+- Fundamental Theorem of Algebra
+
+  A proof that every non-constant polynomial on the complex
+  plane has at least one root
+
+- Real Calculus
+
+  A collection of elementary results on real analysis,
+  including continuity, differentiability, integration,
+  Taylor's theorem and the Fundamental Theorem of Calculus
+
+- Exact Real Computation
+
+  Fast verified computation inside Coq. This includes: real numbers, functions,
+  integrals, graphs of functions, differential equations.
+"""
+
+build: [
+  ["./configure.sh"]
+  [make "-j%{jobs}%"]
+]
+install: [make "install"]
+depends: [
+  "coq" {>= "8.18" & < "8.21~"}
+  "coq-math-classes" {>= "8.19.0"}
+  "coq-bignums" 
+  "coq-elpi" {>= "1.19.3"}
+]
+
+tags: [
+  "category:Mathematics/Algebra"
+  "category:Mathematics/Real Calculus and Topology"
+  "category:Mathematics/Exact Real computation"
+  "keyword:constructive mathematics"
+  "keyword:algebra"
+  "keyword:real calculus"
+  "keyword:real numbers"
+  "keyword:Fundamental Theorem of Algebra"
+  "logpath:CoRN"
+  "date:2025-01-27"
+]
+authors: [
+  "Evgeny Makarov"
+  "Robbert Krebbers"
+  "Eelis van der Weegen"
+  "Bas Spitters"
+  "Jelle Herold"
+  "Russell O'Connor"
+  "Cezary Kaliszyk"
+  "Dan Synek"
+  "Luís Cruz-Filipe"
+  "Milad Niqui"
+  "Iris Loeb"
+  "Herman Geuvers"
+  "Randy Pollack"
+  "Freek Wiedijk"
+  "Jan Zwanenburg"
+  "Dimitri Hendriks"
+  "Henk Barendregt"
+  "Mariusz Giero"
+  "Rik van Ginneken"
+  "Dimitri Hendriks"
+  "Sébastien Hinderer"
+  "Bart Kirkels"
+  "Pierre Letouzey"
+  "Lionel Mamane"
+  "Nickolay Shmyrev"
+  "Vincent Semeria"
+]
+
+url {
+  src: "https://github.com/coq-community/corn/archive/refs/tags/8.20.0.tar.gz"
+  checksum: "sha512=f3dbb1a11deb92483d7db9c5de1a0a33b20594a8da011e31e54cc68e86c8515a29f213a99409778aee26dea74c1f3663b09fe09a528988918856d555b59c4e09"
+}

package_picks/package-pick-8.12.sh

@@ -12,7 +12,7 @@
 
 # The two lines below are used by the package selection script
 COQ_PLATFORM_VERSION_TITLE="Coq 8.12.2 (released Dec 2020) with the first package pick from Dec 2020"
-COQ_PLATFORM_VERSION_SORTORDER=8
+COQ_PLATFORM_VERSION_SORTORDER=9
 
 # The package list name is the final part of the opam switch name.
 # It is usually either empty ot starts with ~.

package_picks/package-pick-8.13~2021.02.sh

@@ -12,7 +12,7 @@
 
 # The two lines below are used by the package selection script
 COQ_PLATFORM_VERSION_TITLE="Coq 8.13.2 (released Apr 2021) with the first package pick from Feb 2021"
-COQ_PLATFORM_VERSION_SORTORDER=7
+COQ_PLATFORM_VERSION_SORTORDER=8
 
 # The package list name is the final part of the opam switch name.
 # It is usually either empty ot starts with ~.

package_picks/package-pick-8.14~2022.01.sh

@@ -12,7 +12,7 @@
 
 # The two lines below are used by the package selection script
 COQ_PLATFORM_VERSION_TITLE="Coq 8.14.1 (released Nov 2021) with the first package pick from Jan 2022"
-COQ_PLATFORM_VERSION_SORTORDER=6
+COQ_PLATFORM_VERSION_SORTORDER=7
 
 # The package list name is the final part of the opam switch name.
 # It is usually either empty ot starts with ~.

package_picks/package-pick-8.15~2022.04.sh

@@ -12,7 +12,7 @@
 
 # The two lines below are used by the package selection script
 COQ_PLATFORM_VERSION_TITLE="Coq 8.15.2 (released Jun 2022) with the first package pick from Apr 2022"
-COQ_PLATFORM_VERSION_SORTORDER=5
+COQ_PLATFORM_VERSION_SORTORDER=6
 
 # The package list name is the final part of the opam switch name.
 # It is usually either empty ot starts with ~.

package_picks/package-pick-8.16~2022.09.sh

@@ -12,7 +12,7 @@
 
 # The two lines below are used by the package selection script
 COQ_PLATFORM_VERSION_TITLE="Coq 8.16.1 (released Nov 2022) with the first package pick from Sep 2022"
-COQ_PLATFORM_VERSION_SORTORDER=4
+COQ_PLATFORM_VERSION_SORTORDER=5
 
 # The package list name is the final part of the opam switch name.
 # It is usually either empty ot starts with ~.

package_picks/package-pick-8.17~2023.08.sh

@@ -12,7 +12,7 @@
 
 # The two lines below are used by the package selection script
 COQ_PLATFORM_VERSION_TITLE="Coq 8.17.1 (released Jun 2023) with the first package pick from Aug 2023"
-COQ_PLATFORM_VERSION_SORTORDER=3
+COQ_PLATFORM_VERSION_SORTORDER=4
 
 # The package list name is the final part of the opam switch name.
 # It is usually either empty ot starts with ~.

package_picks/package-pick-8.18~2023.11.sh

@@ -12,7 +12,7 @@
 
 # The two lines below are used by the package selection script
 COQ_PLATFORM_VERSION_TITLE="Coq 8.18.0 (released Sep 2023) with the first package pick from Nov 2023"
-COQ_PLATFORM_VERSION_SORTORDER=2
+COQ_PLATFORM_VERSION_SORTORDER=3
 
 # The package list name is the final part of the opam switch name.
 # It is usually either empty ot starts with ~.

package_picks/package-pick-8.19~2024.10.sh

@@ -12,7 +12,7 @@
 
 # The two lines below are used by the package selection script
 COQ_PLATFORM_VERSION_TITLE="Coq 8.19.2 (released Jun 2024) with the first package pick from Oct 2024"
-COQ_PLATFORM_VERSION_SORTORDER=1
+COQ_PLATFORM_VERSION_SORTORDER=2
 
 # The package list name is the final part of the opam switch name.
 # It is usually either empty ot starts with ~.
@@ -29,7 +29,6 @@ COQ_PLATFORM_USE_DEV_REPOSITORY='N'
 
 # This extended descriptions is used for readme files
 COQ_PLATFORM_VERSION_DESCRIPTION='This version of Coq Platform 2024.10.1 includes Coq 8.19.2 from Jun 2024. '
-COQ_PLATFORM_VERSION_DESCRIPTION+='This is the **latest release version** of the Coq Platform and recommended for general application. '
 
 # The OCaml version to use for this pick (just the version number - options are elaborated in a platform dependent way)
 COQ_PLATFORM_OCAML_VERSION='4.14.2'
@@ -61,6 +60,7 @@ PACKAGES="${PACKAGES} PIN.coq.8.19.2"
 if  [[ "${COQ_PLATFORM_EXTENT}"  =~ ^[iIfFxX] ]]
 then
 PACKAGES="${PACKAGES} coqide.8.19.2"
+PACKAGES="${PACKAGES} vscoq-language-server.2.2.3"
 fi
 
 ########## "FULL" COQ PLATFORM PACKAGES ##########

package_picks/package-pick-8.20~2025.01.sh

@@ -11,8 +11,8 @@
 ###################### CONTROL VARIABLES #####################
 
 # The two lines below are used by the package selection script
-COQ_PLATFORM_VERSION_TITLE="Coq 8.20.0 (released Sep 2024) with an incomplete preview package pick"
-COQ_PLATFORM_VERSION_SORTORDER=90
+COQ_PLATFORM_VERSION_TITLE="Coq 8.20.1 (released Jan 2025) with the first package pick from Jan 2025"
+COQ_PLATFORM_VERSION_SORTORDER=1
 
 # The package list name is the final part of the opam switch name.
 # It is usually either empty ot starts with ~.
@@ -22,14 +22,14 @@ COQ_PLATFORM_PACKAGE_PICK_POSTFIX='~8.20~2025.01'
 
 # The corresponding Coq development branch and tag
 COQ_PLATFORM_COQ_BRANCH='v8.20'
-COQ_PLATFORM_COQ_TAG='8.20.0'
+COQ_PLATFORM_COQ_TAG='8.20.1'
 
 # This controls if opam repositories for development packages are selected
 COQ_PLATFORM_USE_DEV_REPOSITORY='N'
 
 # This extended descriptions is used for readme files
-COQ_PLATFORM_VERSION_DESCRIPTION='This version of Coq Platform 2025.01.0 includes Coq 8.20.0 from Sep 2024. '
-COQ_PLATFORM_VERSION_DESCRIPTION+='This is a **yet incomplete preview pick** intended for package maintainers and early adopters. '
+COQ_PLATFORM_VERSION_DESCRIPTION='This version of Coq Platform 2025.01.0 includes Coq 8.20.1 from Jan 2025. '
+COQ_PLATFORM_VERSION_DESCRIPTION+='This is the **latest release version** of the Coq Platform and recommended for general application. '
 
 # The OCaml version to use for this pick (just the version number - options are elaborated in a platform dependent way)
 COQ_PLATFORM_OCAML_VERSION='4.14.2'
@@ -52,14 +52,15 @@ PACKAGES="${PACKAGES} PIN.ocamlfind.1.9.5~relocatable"  # TODO port patch to 1.9
 PACKAGES="${PACKAGES} PIN.dune.3.16.1" # Note: 3.17.0 has issues on Windows
 PACKAGES="${PACKAGES} PIN.dune-configurator.3.16.1"
 # The Coq compiler coqc and the Coq standard library
-PACKAGES="${PACKAGES} PIN.coq.8.20.0"
+PACKAGES="${PACKAGES} PIN.coq.8.20.1"
 
 ########## IDE PACKAGES ##########
 
 # GTK based IDE for Coq - alternatives are VSCoq and Proofgeneral for Emacs
 if  [[ "${COQ_PLATFORM_EXTENT}"  =~ ^[iIfFxX] ]]
 then
-PACKAGES="${PACKAGES} coqide.8.20.0"
+PACKAGES="${PACKAGES} coqide.8.20.1"
+PACKAGES="${PACKAGES} vscoq-language-server.2.2.3"
 fi
 
 ########## "FULL" COQ PLATFORM PACKAGES ##########
@@ -94,7 +95,7 @@ then
 
   # Number theory
   PACKAGES="${PACKAGES} coq-coqprime.1.6.0"
-  PACKAGES="${PACKAGES} coq-coqprime-generator.1.1.1" # Note: there is a newer version 1.1.2, but it requires Ocaml 5.X
+  PACKAGES="${PACKAGES} coq-coqprime-generator.1.1.2"
 
   # Numerical mathematics
   PACKAGES="${PACKAGES} coq-flocq.4.2.0"
@@ -104,7 +105,7 @@ then
 
   # Constructive mathematics
   PACKAGES="${PACKAGES} coq-math-classes.8.19.0"
-  PACKAGES="${PACKAGES} coq-corn.8.19.0"
+  PACKAGES="${PACKAGES} coq-corn.8.20.0"
 
   # Homotopy Type Theory (HoTT)
   PACKAGES="${PACKAGES} coq-hott.8.20"

shell_scripts/check_system.sh

@@ -78,7 +78,6 @@ then
 		ls -lL /etc/pki/tls/certs/
 		echo "============ Fix certificate database done ============"
 	fi
-
 else
 		echo "ERROR: unsopported OS type '$OSTYPE'"
 		return 1

shell_scripts/post_system.sh

@@ -0,0 +1,18 @@
+#!/bin/bash
+
+###################### COPYRIGHT/COPYLEFT ######################
+
+# (C) 2025 Michael Soegtrop
+
+# Released to the public under the
+# Creative Commons CC0 1.0 Universal License
+# See https://creativecommons.org/publicdomain/zero/1.0/legalcode.txt
+
+###################### POST CHECKS / FIXES #####################
+
+if [[ "$OSTYPE" == cygwin ]]
+then
+  # Call the script to link shared libraries into the bin folder.
+  # This is required e.g. to call vscoqtop from VSCoq without setting PATH.
+  /platform/windows/link_shared_libraries.sh
+fi

windows/configure_profile.sh

@@ -43,6 +43,13 @@ if [ ! -f $donefile ] ; then
   echo export OPAMROOT="'$(cygpath -aw /opam)'"
   echo export PLATFORMROOT="'$(cygpath -aw /platform)'"
 
+  # Disable sandboxing in dune
+	# On Cygwin it works better to disable dune sandboxing.
+	# Sometimes virus checkers interfer with this, which makes the build unreliable.
+	# See https://dune.readthedocs.io/en/stable/reference/config/sandboxing_preference.html
+	# See https://dune.readthedocs.io/en/stable/concepts/sandboxing.html
+  echo export DUNE_SANDBOX=none
+
   exec 1>&6 6>&-       # Restore stdout from file descriptor 6 and close file descriptor #6
 
   touch $donefile

windows/create_installer_windows.sh

@@ -22,11 +22,20 @@ HERE="$(pwd)"
 
 source shell_scripts/installer_utilities.sh
 
+##### Check if hard links for external use have been created #####
+
+if [ -f "/platform/windows/link_shared_libraries_undo.sh" ]
+then
+  echo "WARNING: removing hard links for external use of this cygwin installation"
+  echo "WARNING: this will break e.g. VSCoq"
+  echo "To restore the links call /platform/windows/link_shared_libraries.sh"
+  /platform/windows/link_shared_libraries_undo.sh
+fi
+
 ##### Get the release and package pick of the Coq Platform #####
 
 source shell_scripts/get_names_from_switch.sh
 
-
 ###### Create root folder #####
 
 DIR_TARGET=windows_installer