Skip to content

Commit 4475633

Browse files
MSoegtropIMCMSoegtropIMC
authored
Merge pull request #463 from MSoegtropIMC/2025.01-prep-8
2025.01 prep 8
2 parents 0bcba70 + 2c36c3d commit 4475633

17 files changed

+277
-20
lines changed

Diff for: ‎coq_platform_make.sh

+4
Original file line numberDiff line numberDiff line change
@@ -76,6 +76,10 @@ source shell_scripts/install_system_prerequisites.sh
7676

7777
source shell_scripts/build.sh
7878

79+
###################### FINALIZE #####################
80+
81+
source shell_scripts/post_system.sh
82+
7983
###################### CLOSING #####################
8084

8185
source shell_scripts/closing_remarks.sh

Diff for: ‎opam/opam-coq-archive/released/packages/coq-coqprime-generator/coq-coqprime-generator.1.1.2/opam

+45
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,45 @@
1+
opam-version: "2.0"
2+
maintainer: "[email protected]"
3+
homepage: "https://github.com/thery/coqprime"
4+
bug-reports: "https://github.com/thery/coqprime/issues"
5+
dev-repo: "git+https://github.com/thery/coqprime.git"
6+
license: "LGPL-2.1-only"
7+
authors: ["Laurent Théry"]
8+
9+
build: [
10+
# cd to a subfolder in opam is tricky, so just move gencertif to the root folder
11+
[ "find" "gencertif" "-type" "f" "-exec" "mv" "{}" "." ";" ]
12+
[ "autoreconf" "-i" "-s" ]
13+
[ "./configure" "--prefix" prefix
14+
# Optiosn for finding opam local gmp-ecm
15+
"CPPFLAGS=-I%{prefix}%/include"
16+
"LDFLAGS=-L%{lib}%"
17+
# Options for homebrew on Intel silicon (overwriting the above)
18+
"CPPFLAGS=-I%{prefix}%/include -I/opt/local/include" { os-distribution = "macports" & os = "macos" }
19+
"LDFLAGS=-L%{lib}% -L/opt/local/lib" { os-distribution = "macports" & os = "macos" }
20+
# Options for homebrew on Apple silicon (overwriting the above)
21+
"CPPFLAGS=-I%{prefix}%/include -I/opt/homebrew/include" { os-distribution = "homebrew" & os = "macos" & arch = "arm64"}
22+
"LDFLAGS=-L%{lib}% -L/opt/homebrew/lib" { os-distribution = "homebrew" & os = "macos" & arch = "arm64"}
23+
# Options for Windows cygwin
24+
"--build=%{arch}%-pc-cygwin" { os = "win32" & os-distribution = "cygwinports" }
25+
"--host=%{arch}%-w64-mingw32" { os = "win32" & os-distribution = "cygwinports" }
26+
"--target=%{arch}%-w64-mingw32" { os = "win32" & os-distribution = "cygwinports" }
27+
]
28+
[ make "-j" "%{jobs}%" ]
29+
]
30+
install: [
31+
[make "install"]
32+
]
33+
depends: [
34+
"ocaml" {>= "4.14.2"}
35+
"ocamlfind"
36+
"zarith"
37+
"num"
38+
"conf-gmp"
39+
"gmp-ecm"
40+
]
41+
synopsis: "Certificate generator for prime numbers in Coq"
42+
url {
43+
src: "https://github.com/thery/coqprime/archive/v8.20.1.tar.gz"
44+
checksum: "sha512=8281e395b919fff9244287a75b2ab3ade21fc989e22185c4eb788706cc6a099a4be3de4435bdf60e5da32824a500b642ad8f7b759f2c4ddf0359f2d438413e68"
45+
}

Diff for: ‎opam/opam-coq-archive/released/packages/coq-corn/coq-corn.8.20.0/opam

+98
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,98 @@
1+
opam-version: "2.0"
2+
maintainer: "[email protected]"
3+
4+
homepage: "https://github.com/coq-community/corn"
5+
dev-repo: "git+https://github.com/coq-community/corn.git"
6+
bug-reports: "https://github.com/coq-community/corn/issues"
7+
license: "GPL-2.0"
8+
9+
synopsis: "The Coq Constructive Repository at Nijmegen"
10+
description: """
11+
CoRN includes the following parts:
12+
13+
- Algebraic Hierarchy
14+
15+
An axiomatic formalization of the most common algebraic
16+
structures, including setoids, monoids, groups, rings,
17+
fields, ordered fields, rings of polynomials, real and
18+
complex numbers
19+
20+
- Model of the Real Numbers
21+
22+
Construction of a concrete real number structure
23+
satisfying the previously defined axioms
24+
25+
- Fundamental Theorem of Algebra
26+
27+
A proof that every non-constant polynomial on the complex
28+
plane has at least one root
29+
30+
- Real Calculus
31+
32+
A collection of elementary results on real analysis,
33+
including continuity, differentiability, integration,
34+
Taylor's theorem and the Fundamental Theorem of Calculus
35+
36+
- Exact Real Computation
37+
38+
Fast verified computation inside Coq. This includes: real numbers, functions,
39+
integrals, graphs of functions, differential equations.
40+
"""
41+
42+
build: [
43+
["./configure.sh"]
44+
[make "-j%{jobs}%"]
45+
]
46+
install: [make "install"]
47+
depends: [
48+
"coq" {>= "8.18" & < "8.21~"}
49+
"coq-math-classes" {>= "8.19.0"}
50+
"coq-bignums"
51+
"coq-elpi" {>= "1.19.3"}
52+
]
53+
54+
tags: [
55+
"category:Mathematics/Algebra"
56+
"category:Mathematics/Real Calculus and Topology"
57+
"category:Mathematics/Exact Real computation"
58+
"keyword:constructive mathematics"
59+
"keyword:algebra"
60+
"keyword:real calculus"
61+
"keyword:real numbers"
62+
"keyword:Fundamental Theorem of Algebra"
63+
"logpath:CoRN"
64+
"date:2025-01-27"
65+
]
66+
authors: [
67+
"Evgeny Makarov"
68+
"Robbert Krebbers"
69+
"Eelis van der Weegen"
70+
"Bas Spitters"
71+
"Jelle Herold"
72+
"Russell O'Connor"
73+
"Cezary Kaliszyk"
74+
"Dan Synek"
75+
"Luís Cruz-Filipe"
76+
"Milad Niqui"
77+
"Iris Loeb"
78+
"Herman Geuvers"
79+
"Randy Pollack"
80+
"Freek Wiedijk"
81+
"Jan Zwanenburg"
82+
"Dimitri Hendriks"
83+
"Henk Barendregt"
84+
"Mariusz Giero"
85+
"Rik van Ginneken"
86+
"Dimitri Hendriks"
87+
"Sébastien Hinderer"
88+
"Bart Kirkels"
89+
"Pierre Letouzey"
90+
"Lionel Mamane"
91+
"Nickolay Shmyrev"
92+
"Vincent Semeria"
93+
]
94+
95+
url {
96+
src: "https://github.com/coq-community/corn/archive/refs/tags/8.20.0.tar.gz"
97+
checksum: "sha512=f3dbb1a11deb92483d7db9c5de1a0a33b20594a8da011e31e54cc68e86c8515a29f213a99409778aee26dea74c1f3663b09fe09a528988918856d555b59c4e09"
98+
}

Diff for: ‎package_picks/package-pick-8.12.sh

+1-1
Original file line numberDiff line numberDiff line change
@@ -12,7 +12,7 @@
1212

1313
# The two lines below are used by the package selection script
1414
COQ_PLATFORM_VERSION_TITLE="Coq 8.12.2 (released Dec 2020) with the first package pick from Dec 2020"
15-
COQ_PLATFORM_VERSION_SORTORDER=8
15+
COQ_PLATFORM_VERSION_SORTORDER=9
1616

1717
# The package list name is the final part of the opam switch name.
1818
# It is usually either empty ot starts with ~.

Diff for: ‎package_picks/package-pick-8.13~2021.02.sh

+1-1
Original file line numberDiff line numberDiff line change
@@ -12,7 +12,7 @@
1212

1313
# The two lines below are used by the package selection script
1414
COQ_PLATFORM_VERSION_TITLE="Coq 8.13.2 (released Apr 2021) with the first package pick from Feb 2021"
15-
COQ_PLATFORM_VERSION_SORTORDER=7
15+
COQ_PLATFORM_VERSION_SORTORDER=8
1616

1717
# The package list name is the final part of the opam switch name.
1818
# It is usually either empty ot starts with ~.

Diff for: ‎package_picks/package-pick-8.14~2022.01.sh

+1-1
Original file line numberDiff line numberDiff line change
@@ -12,7 +12,7 @@
1212

1313
# The two lines below are used by the package selection script
1414
COQ_PLATFORM_VERSION_TITLE="Coq 8.14.1 (released Nov 2021) with the first package pick from Jan 2022"
15-
COQ_PLATFORM_VERSION_SORTORDER=6
15+
COQ_PLATFORM_VERSION_SORTORDER=7
1616

1717
# The package list name is the final part of the opam switch name.
1818
# It is usually either empty ot starts with ~.

Diff for: ‎package_picks/package-pick-8.15~2022.04.sh

+1-1
Original file line numberDiff line numberDiff line change
@@ -12,7 +12,7 @@
1212

1313
# The two lines below are used by the package selection script
1414
COQ_PLATFORM_VERSION_TITLE="Coq 8.15.2 (released Jun 2022) with the first package pick from Apr 2022"
15-
COQ_PLATFORM_VERSION_SORTORDER=5
15+
COQ_PLATFORM_VERSION_SORTORDER=6
1616

1717
# The package list name is the final part of the opam switch name.
1818
# It is usually either empty ot starts with ~.

Diff for: ‎package_picks/package-pick-8.16~2022.09.sh

+1-1
Original file line numberDiff line numberDiff line change
@@ -12,7 +12,7 @@
1212

1313
# The two lines below are used by the package selection script
1414
COQ_PLATFORM_VERSION_TITLE="Coq 8.16.1 (released Nov 2022) with the first package pick from Sep 2022"
15-
COQ_PLATFORM_VERSION_SORTORDER=4
15+
COQ_PLATFORM_VERSION_SORTORDER=5
1616

1717
# The package list name is the final part of the opam switch name.
1818
# It is usually either empty ot starts with ~.

Diff for: ‎package_picks/package-pick-8.17~2023.08.sh

+1-1
Original file line numberDiff line numberDiff line change
@@ -12,7 +12,7 @@
1212

1313
# The two lines below are used by the package selection script
1414
COQ_PLATFORM_VERSION_TITLE="Coq 8.17.1 (released Jun 2023) with the first package pick from Aug 2023"
15-
COQ_PLATFORM_VERSION_SORTORDER=3
15+
COQ_PLATFORM_VERSION_SORTORDER=4
1616

1717
# The package list name is the final part of the opam switch name.
1818
# It is usually either empty ot starts with ~.

Diff for: ‎package_picks/package-pick-8.18~2023.11.sh

+1-1
Original file line numberDiff line numberDiff line change
@@ -12,7 +12,7 @@
1212

1313
# The two lines below are used by the package selection script
1414
COQ_PLATFORM_VERSION_TITLE="Coq 8.18.0 (released Sep 2023) with the first package pick from Nov 2023"
15-
COQ_PLATFORM_VERSION_SORTORDER=2
15+
COQ_PLATFORM_VERSION_SORTORDER=3
1616

1717
# The package list name is the final part of the opam switch name.
1818
# It is usually either empty ot starts with ~.

Diff for: ‎package_picks/package-pick-8.19~2024.10.sh

+2-2
Original file line numberDiff line numberDiff line change
@@ -12,7 +12,7 @@
1212

1313
# The two lines below are used by the package selection script
1414
COQ_PLATFORM_VERSION_TITLE="Coq 8.19.2 (released Jun 2024) with the first package pick from Oct 2024"
15-
COQ_PLATFORM_VERSION_SORTORDER=1
15+
COQ_PLATFORM_VERSION_SORTORDER=2
1616

1717
# The package list name is the final part of the opam switch name.
1818
# It is usually either empty ot starts with ~.
@@ -29,7 +29,6 @@ COQ_PLATFORM_USE_DEV_REPOSITORY='N'
2929

3030
# This extended descriptions is used for readme files
3131
COQ_PLATFORM_VERSION_DESCRIPTION='This version of Coq Platform 2024.10.1 includes Coq 8.19.2 from Jun 2024. '
32-
COQ_PLATFORM_VERSION_DESCRIPTION+='This is the **latest release version** of the Coq Platform and recommended for general application. '
3332

3433
# The OCaml version to use for this pick (just the version number - options are elaborated in a platform dependent way)
3534
COQ_PLATFORM_OCAML_VERSION='4.14.2'
@@ -61,6 +60,7 @@ PACKAGES="${PACKAGES} PIN.coq.8.19.2"
6160
if [[ "${COQ_PLATFORM_EXTENT}" =~ ^[iIfFxX] ]]
6261
then
6362
PACKAGES="${PACKAGES} coqide.8.19.2"
63+
PACKAGES="${PACKAGES} vscoq-language-server.2.2.3"
6464
fi
6565

6666
########## "FULL" COQ PLATFORM PACKAGES ##########

Diff for: ‎package_picks/package-pick-8.20~2025.01.sh

+10-9
Original file line numberDiff line numberDiff line change
@@ -11,8 +11,8 @@
1111
###################### CONTROL VARIABLES #####################
1212

1313
# The two lines below are used by the package selection script
14-
COQ_PLATFORM_VERSION_TITLE="Coq 8.20.0 (released Sep 2024) with an incomplete preview package pick"
15-
COQ_PLATFORM_VERSION_SORTORDER=90
14+
COQ_PLATFORM_VERSION_TITLE="Coq 8.20.1 (released Jan 2025) with the first package pick from Jan 2025"
15+
COQ_PLATFORM_VERSION_SORTORDER=1
1616

1717
# The package list name is the final part of the opam switch name.
1818
# It is usually either empty ot starts with ~.
@@ -22,14 +22,14 @@ COQ_PLATFORM_PACKAGE_PICK_POSTFIX='~8.20~2025.01'
2222

2323
# The corresponding Coq development branch and tag
2424
COQ_PLATFORM_COQ_BRANCH='v8.20'
25-
COQ_PLATFORM_COQ_TAG='8.20.0'
25+
COQ_PLATFORM_COQ_TAG='8.20.1'
2626

2727
# This controls if opam repositories for development packages are selected
2828
COQ_PLATFORM_USE_DEV_REPOSITORY='N'
2929

3030
# This extended descriptions is used for readme files
31-
COQ_PLATFORM_VERSION_DESCRIPTION='This version of Coq Platform 2025.01.0 includes Coq 8.20.0 from Sep 2024. '
32-
COQ_PLATFORM_VERSION_DESCRIPTION+='This is a **yet incomplete preview pick** intended for package maintainers and early adopters. '
31+
COQ_PLATFORM_VERSION_DESCRIPTION='This version of Coq Platform 2025.01.0 includes Coq 8.20.1 from Jan 2025. '
32+
COQ_PLATFORM_VERSION_DESCRIPTION+='This is the **latest release version** of the Coq Platform and recommended for general application. '
3333

3434
# The OCaml version to use for this pick (just the version number - options are elaborated in a platform dependent way)
3535
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
5252
PACKAGES="${PACKAGES} PIN.dune.3.16.1" # Note: 3.17.0 has issues on Windows
5353
PACKAGES="${PACKAGES} PIN.dune-configurator.3.16.1"
5454
# The Coq compiler coqc and the Coq standard library
55-
PACKAGES="${PACKAGES} PIN.coq.8.20.0"
55+
PACKAGES="${PACKAGES} PIN.coq.8.20.1"
5656

5757
########## IDE PACKAGES ##########
5858

5959
# GTK based IDE for Coq - alternatives are VSCoq and Proofgeneral for Emacs
6060
if [[ "${COQ_PLATFORM_EXTENT}" =~ ^[iIfFxX] ]]
6161
then
62-
PACKAGES="${PACKAGES} coqide.8.20.0"
62+
PACKAGES="${PACKAGES} coqide.8.20.1"
63+
PACKAGES="${PACKAGES} vscoq-language-server.2.2.3"
6364
fi
6465

6566
########## "FULL" COQ PLATFORM PACKAGES ##########
@@ -94,7 +95,7 @@ then
9495

9596
# Number theory
9697
PACKAGES="${PACKAGES} coq-coqprime.1.6.0"
97-
PACKAGES="${PACKAGES} coq-coqprime-generator.1.1.1" # Note: there is a newer version 1.1.2, but it requires Ocaml 5.X
98+
PACKAGES="${PACKAGES} coq-coqprime-generator.1.1.2"
9899

99100
# Numerical mathematics
100101
PACKAGES="${PACKAGES} coq-flocq.4.2.0"
@@ -104,7 +105,7 @@ then
104105

105106
# Constructive mathematics
106107
PACKAGES="${PACKAGES} coq-math-classes.8.19.0"
107-
PACKAGES="${PACKAGES} coq-corn.8.19.0"
108+
PACKAGES="${PACKAGES} coq-corn.8.20.0"
108109

109110
# Homotopy Type Theory (HoTT)
110111
PACKAGES="${PACKAGES} coq-hott.8.20"

Diff for: ‎shell_scripts/check_system.sh

-1
Original file line numberDiff line numberDiff line change
@@ -78,7 +78,6 @@ then
7878
ls -lL /etc/pki/tls/certs/
7979
echo "============ Fix certificate database done ============"
8080
fi
81-
8281
else
8382
echo "ERROR: unsopported OS type '$OSTYPE'"
8483
return 1

Diff for: ‎shell_scripts/post_system.sh

+18
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,18 @@
1+
#!/bin/bash
2+
3+
###################### COPYRIGHT/COPYLEFT ######################
4+
5+
# (C) 2025 Michael Soegtrop
6+
7+
# Released to the public under the
8+
# Creative Commons CC0 1.0 Universal License
9+
# See https://creativecommons.org/publicdomain/zero/1.0/legalcode.txt
10+
11+
###################### POST CHECKS / FIXES #####################
12+
13+
if [[ "$OSTYPE" == cygwin ]]
14+
then
15+
# Call the script to link shared libraries into the bin folder.
16+
# This is required e.g. to call vscoqtop from VSCoq without setting PATH.
17+
/platform/windows/link_shared_libraries.sh
18+
fi

Diff for: ‎windows/configure_profile.sh

+7
Original file line numberDiff line numberDiff line change
@@ -43,6 +43,13 @@ if [ ! -f $donefile ] ; then
4343
echo export OPAMROOT="'$(cygpath -aw /opam)'"
4444
echo export PLATFORMROOT="'$(cygpath -aw /platform)'"
4545

46+
# Disable sandboxing in dune
47+
# On Cygwin it works better to disable dune sandboxing.
48+
# Sometimes virus checkers interfer with this, which makes the build unreliable.
49+
# See https://dune.readthedocs.io/en/stable/reference/config/sandboxing_preference.html
50+
# See https://dune.readthedocs.io/en/stable/concepts/sandboxing.html
51+
echo export DUNE_SANDBOX=none
52+
4653
exec 1>&6 6>&- # Restore stdout from file descriptor 6 and close file descriptor #6
4754

4855
touch $donefile

Diff for: ‎windows/create_installer_windows.sh

+10-1
Original file line numberDiff line numberDiff line change
@@ -22,11 +22,20 @@ HERE="$(pwd)"
2222

2323
source shell_scripts/installer_utilities.sh
2424

25+
##### Check if hard links for external use have been created #####
26+
27+
if [ -f "/platform/windows/link_shared_libraries_undo.sh" ]
28+
then
29+
echo "WARNING: removing hard links for external use of this cygwin installation"
30+
echo "WARNING: this will break e.g. VSCoq"
31+
echo "To restore the links call /platform/windows/link_shared_libraries.sh"
32+
/platform/windows/link_shared_libraries_undo.sh
33+
fi
34+
2535
##### Get the release and package pick of the Coq Platform #####
2636

2737
source shell_scripts/get_names_from_switch.sh
2838

29-
3039
###### Create root folder #####
3140

3241
DIR_TARGET=windows_installer

0 commit comments

Comments
 (0)