Skip to content

bum coq-hott to 9.1 localy waiting opam package and add PIN rocq-core #529

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Open
Justme0606 wants to merge 1 commit into
base: main
Choose a base branch
from
+33 −3
Open

bum coq-hott to 9.1 localy waiting opam package and add PIN rocq-core #529

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
1 commit
Select commit
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
28 changes: 28 additions & 0 deletions opam/opam-coq-archive/released/packages/coq-hott/coq-hott.9.1/opam
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -0,0 +1,28 @@
opam-version: "2.0"
maintainer: [ "Jason Gross <jgross@mit.edu>" "Ali Caglayan <alizter@gmail.com>" ]
homepage: "http://homotopytypetheory.org/"
bug-reports: "https://github.com/HoTT/HoTT/issues"
license: "BSD-2-Clause"
build: [ "dune" "build" "-p" name "-j" jobs "@install" ]
install: [ "dune" "install" "-p" name ]
depends: [
"ocaml" {>= "4.14"}
"dune" {>= "3.13"}
(("rocq-core" {>= "9.0" & < "9.2~"} & "coq-core" {>= "9.0" & < "9.2~"})
| "coq" {>= "8.19.0" & < "9.2~"})
]
authors: ["The HoTT Library Development Team"]
dev-repo: "git+https://github.com/HoTT/HoTT.git"
synopsis: "The Homotopy Type Theory library"
description: """
To use the HoTT library, the following flags must be passed to coqc:
-noinit -indices-matter
To use the HoTT library in a project, add the following to _CoqProject:
-arg -noinit
-arg -indices-matter
"""
tags: [ "logpath:HoTT" ]
url {
src: "https://github.com/HoTT/Coq-HoTT/archive/refs/tags/V9.1.tar.gz"
checksum: "sha512=134caf34ea9353967325699fc211b7df0eb32654b34b70c8eed321da3da937b45e823c5e925058840593c9cb3c26617dac945a3e64d2cf04e9d9bc9216d7616d"
}
8 changes: 5 additions & 3 deletions package_picks/package-pick-9.1~2026.01.sh
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -52,6 +52,8 @@ PACKAGES="${PACKAGES} PIN.ocamlfind.1.9.8+relocatable" # TODO port patch to 1.9.
PACKAGES="${PACKAGES} PIN.dune.3.21.0" # 3.17.2 has issues on Windows: cairo doesn't find cairo.h
PACKAGES="${PACKAGES} PIN.dune-configurator.3.21.0"
# The Coq compiler coqc and the Coq standard library
PACKAGES="${PACKAGES} PIN.rocq-runtime.9.1.0"
PACKAGES="${PACKAGES} PIN.rocq-core.9.1.0"
PACKAGES="${PACKAGES} PIN.coq.9.1.0"
PACKAGES="${PACKAGES} PIN.rocq-stdlib.9.0.0" # modified after discuted with Théo to bump to 9.1.0
# Tester avec 9.0.0, avoir une version qui marche et ensuite bump et voir le nombre de paquets qui sont cassés.
Expand Down Expand Up @@ -112,7 +114,7 @@ then
PACKAGES="${PACKAGES} coq-corn.9.0.0"

# Homotopy Type Theory (HoTT)
#PACKAGES="${PACKAGES} coq-hott.9.0" # error compilation
PACKAGES="${PACKAGES} coq-hott.9.1" # error compilation

# Univalent Mathematics (UniMath)
# Note: coq-unimath requires too much memory for 32 bit architectures
Expand All @@ -133,8 +135,8 @@ then
PACKAGES="${PACKAGES} coq-menhirlib.20250903 menhir.20250903" # modified
PACKAGES="${PACKAGES} rocq-equations.1.3.1+9.1" # modified
PACKAGES="${PACKAGES} rocq-aac-tactics.9.0.0"
PACKAGES="${PACKAGES} coq-unicoq.1.6+9.1" # modified
PACKAGES="${PACKAGES} coq-mtac2.1.4+9.1" # modified linked with unicoq
#PACKAGES="${PACKAGES} coq-unicoq.1.6+8.20" # error
#PACKAGES="${PACKAGES} coq-mtac2.1.4+9.0" # error with unicoq
PACKAGES="${PACKAGES} coq-quickchick.2.1.1"
PACKAGES="${PACKAGES} coq-hammer-tactics.1.3.2+9.1" # modified
if [[ "$OSTYPE" != cygwin ]]
Expand Down
Loading