search

HoTT / Coq-HoTT

A Coq library for Homotopy Type Theory
http://homotopytypetheory.org/
Other
1.26k stars 193 forks source link

Informative: pick of tag for upcoming release of Coq Platform for Coq 8.14 #1581

Closed MSoegtropIMC closed 3 years ago

MSoegtropIMC commented 3 years ago

The Coq team released Coq 8.14+rc1 on September 17, 2021 and plans to release Coq 8.14.0 before October 31, 2021. A corresponding Coq Platform releases should be released before November 30, 2021. It can be dealyed in case of difficulties until January 31, 2022, but this should be an exception.

This issue is to inform you that your latest tag does work fine with Coq 8.14+rc1.

Coq Platform currently uses the opam package 'coq-hott.8.13~flex' from platform patch repository https://github.com/coq/platform/tree/main/opam/opam-coq-archive/released.

Note: We had to patch the opam package and possibly the make file to accept the new version of Coq, but no other changes were required.

In case this is the version you want to see in Coq Platform, there is nothing to do for you - just close this issue.

In case you would prefer to see an updated version in the upcoming Coq Platform, please inform as as soon as possible!

Thanks!

P.S.: this issue has been created semi-automatically.

CC: https://github.com/coq/platform/issues/139

Alizter commented 3 years ago

@MSoegtropIMC I intend to make a coq 8.14 HoTT library release soon, we are just waiting for coq to release properly in the mean time.

You mentioned that you had to patch the opam file and the makefile, would you be able to elaborate on what was needed?

MSoegtropIMC commented 3 years ago

I just had to tell in opam "yes this package works with Coq 8.14" - nothing else.

You can find the patched opam file here: (https://github.com/coq/platform/tree/main/opam/opam-coq-archive/released/packages/coq-hott/coq-hott.8.13%7Eflex)

I guess I should change my script to put in a direct link to the opam file rather than a repo link ...

Please let me close the issue - I will do so after I updated to HoTT to the 8.14 release. This is just a measure of "double book keeping" to avoid I ship the wrong package.

Alizter commented 3 years ago

@MSoegtropIMC We now have a v8.14 🏷️

MSoegtropIMC commented 3 years ago

I don't see an opam package as yet. Do you want me to create one?

MSoegtropIMC commented 3 years ago

I created a Coq Platform local opam package - I plan to push it to the opam coq released repo today evening. I will put you on CC on the PR.

MSoegtropIMC commented 3 years ago

Hmm, I can't manage to get the new tag compiled via opam. From your docs I guess that I should now call just "make", but this does not work. I get:

bash etc/generate_coqproject.sh
Warning: Not a git clone, using find instead
coq_makefile -f _CoqProject -o Makefile.coq
/Applications/Xcode.app/Contents/Developer/usr/bin/make --no-print-directory -f Makefile.coq 
COQDEP VFILES
*** Warning: in file theories//Basics/Notations.v, declared ML module ltac_plugin has not been found!
*** Warning: in file theories//Basics/Overture.v, declared ML module number_string_notation_plugin has not been found!
COQC contrib//HoTTBook.v
File "./contrib//HoTTBook.v", line 60, characters 15-19:
Error: Unable to locate library HoTT.

make[2]: *** [contrib//HoTTBook.vo] Error 1
make[1]: *** [all] Error 2
make: *** [invoke-coqmakefile] Error 2

The opam file is

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: [
  [make "-j1"]
]
install: [make "install"]
depends: [
  "ocaml"
  "ocamlfind" {build}
  "coq" {>= "8.13" & < "8.15~"}
]
authors: ["The Coq-HoTT 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/HoTT/archive/refs/tags/V8.14.tar.gz"
  checksum: "sha512=213c909ce04290f885b7605b1b7777a6552c2a4642e7d289a0e1e4b737c625867ad73c6a56c824eba952ff95e8e98a9d78061d8a3c7a8420f7ad3beab62ad87e"
}
MSoegtropIMC commented 3 years ago

@Alizter : attached please find the generated _CoqProject file:

_CoqProject.txt

MSoegtropIMC commented 3 years ago

I updated to "coq-hott.8.14".