Please pick the version you prefer for Coq 8.17 in Coq Platform 2023.03 about coq-hott

[Alizter]

I have a made a release and opened a PR:
coq/opam#2514

[Alizter]

Looks fine to me.

[MSoegtropIMC]

I created coq/opam#2508 to relax the Coq version restriction for coq-hott.8.16 to allow 8.17.

If this is not what you meant, please reopen!

[Alizter]

@MSoegtropIMC Would you be able to choose the current master commit in the release?

[MSoegtropIMC]

@Alizter : the rules of Coq Platform state that we use only proper releases - possibly with minor compatibility patches. So I would definitely need a tag.

[MSoegtropIMC]

But if the question is if I can try the current master commit - yes I can temporarily use a Coq Platform local opam file which links to a commit.

[Alizter]

Let me quickly make a release then.

[MSoegtropIMC]

Thanks! I updated Coq Platform to version 8.17 and close this issue.

[MSoegtropIMC]

Unfortunately my smoke test kit does not run through:

====================== Running test file coq-hott/Locator.v ======================
coqc -noinit -indices-matter Locator.v
File "./Locator.v", line 529, characters 16-21:
Error:
In environment
Q : Type
Aap : Apart Q
Aplus : Plus Q
Amult : Mult Q
Azero : Zero Q
Aone : One Q
Aneg : Negate Q
Arecip : DecRecip Q
Ale : Le Q
Alt : Lt Q
U : RationalsToField Q
Qrats : Rationals Q
Qdec_paths : DecidablePaths Q
Qtriv : TrivialApart Q
Trichotomy0 : Trichotomy lt
F : Type
Alt0 : Lt F
Ale0 : Le F
Aap0 : Apart F
Azero0 : Zero F
Aone0 : One F
Aplus0 : Plus F
Anegate : Negate F
Amult0 : Mult F
Arecip0 : Recip F
Ajoin : Join F
Ameet : Meet F
Forderedfield : OrderedField F
Fabs : Abs F
Farchimedean : ArchimedeanProperty Q F
Fcomplete : IsComplete Q F
Qroundup : RoundUpStrict Q
H : Funext
H0 : Univalence
Q_eq : nat <~> Q
QQpos_eq : nat <~> Q * Qpos Q
cast_pres_ordering : StrictlyOrderPreserving qinc
qinc_strong_presving : IsSemiRingStrongPreserving qinc
x, y : F
l : locator x
m : locator y
ltxy : x < y
Unable to unify "forall qeps' : Q * Qpos Q, Decidable (P qeps')" with
 "forall x : Q * Qpos Q, IsHProp (P x)".

[MSoegtropIMC]

Please hold on this - possibly an error in my testing procedures. I am rechecking ...

[MSoegtropIMC]

Sorry, my bad. I forgot an eval $(opam env). The smoke test kit for HoTT is fine.