Please create a tag for Coq 8.17 in Coq Platform 2023.03 about coqeal HOT 9 CLOSED

After updating coq-mathcomp-real-closed to version 1.1.4, coq-coqeal 1.1.1 indeed compiles fine.

I take your above comment as conformation that this is the version you want in Coq Platform 2023.03 (if not or you change your mind later, please reopen).

from coqeal.

@proux01 : coq-coqeal 1.1.1 compiles fine, but I have issues with the agreed on "smoke test kit" file, which is:

refinements/examples/irred.v

It fails with:

File "./irred.v", line 83, characters 0-41:
Error: The default value for hint locality is currently "local" in a section
and "global" otherwise, but is scheduled to change in a future release. For
the time being, adding hints outside of sections without specifying an
explicit locality attribute is therefore deprecated. It is recommended to use
"export" whenever possible. Use the attributes #[local], #[global] and
#[export] depending on your choice. For example: "#[export] Hint Unfold foo :
bar." [deprecated-hint-without-locality,deprecated]

Can you please have a look?

Having files in a folder named "examples" which don't compile can leave a very bad impression on first time users, so I would recommend to test this in your CI.

from coqeal.

I can give options in the smoke test, but up to now I did not use this to disable warnings. It is currently used for HoTT and Unimath to give -noinit -indices-matter and for 32 bit CompCert and VST to drag in installations from the non standard folders the 32 bit versions end up in.

I think for users things get tricky when examples only compile with (to non experts) non obvious command line parameters, so I try to avoid this as much as possible and prefer if users can just open a file in an IDE without caring for _CoqProject files - it should be sufficient that the respective package is installed via opam.

So IMHO it would be better to fix these warnings rather than to disable them. Likely in 8.18 you anyway have to fix it.

from coqeal.

@MSoegtropIMC coq-coqeal.1.1.1 compiles fine with Coq 8.17 (tested only yesterday, sorry for the delay, this was waiting for the release of coq-real-closed.1.1.4)

from coqeal.

Indeed I don't adjust my messages to the case that a prerequisite does not compile ... I recheck.

from coqeal.

@MSoegtropIMC the file is actually compiled fine along with CoqEAL in the CI, but with options in the _CoqProject which include:

-arg -w -arg -deprecated-hint-without-locality

How do you compile the smoke test? Should I do a new release without that compilation option? (that might be the best solution)

from coqeal.

I agree, so I just released a 1.1.2 for which the smoke test compiles without any specific option on Coq 8.17: coq/opam#2502

from coqeal.

Perfect, thanks - especially for the quick work!

from coqeal.

Thanks! I updated the 2023.03 preview pick to version 1.1.2 and close this issue.

from coqeal.