Ali Caglayan (Apr 04 2022 at 16:59): Ali Caglayan (Apr 04 2022 at 16:59):The patch seems to be a little non-trivial however. Jasmin uses a lot of Let _ := blah in their code, however the vernacular command Let seems to take in an ident whilst let takes in a name which can be an underscore.
Ali Caglayan (Apr 04 2022 at 17:00):Ident was changed to not allow underscores
Ali Caglayan (Apr 04 2022 at 17:00):Changing the Let to let doesn't quite workout in Jasmin however
Ali Caglayan (Apr 04 2022 at 17:01):Should I change Let to take a name rather than an ident?
Ali Caglayan (Apr 04 2022 at 17:07):I guess for now I can patch Jasmin to give a name. It seems strange that we don't want Let _ := foo as valid syntax however.
Ali Caglayan (Apr 04 2022 at 17:07):Perhaps for the best.
Gaëtan Gilbert (Apr 04 2022 at 17:11):Ali Caglayan said:
Should I change Let to take a name rather than an ident?
y
Ali Caglayan (Apr 04 2022 at 17:52):I've done this but now I have an issue
Ali Caglayan (Apr 04 2022 at 17:52):Which is name shadowing
Ali Caglayan (Apr 04 2022 at 17:52):Unnamed_thm already exists.
How can I freshen this name?
Ali Caglayan (Apr 04 2022 at 17:57):Looks like we have in vernacentries:
let default_thm_id = Id.of_string "Unnamed_thm"
let fresh_name_for_anonymous_theorem () =
Namegen.next_global_ident_away default_thm_id Id.Set.empty
Am I reading this wrong or is this quite useless?
Gaëtan Gilbert (Apr 04 2022 at 18:04):it's freshened at the start of the proof instead of at the end so this error can happen with nested proofs
are they using nested proofs?
Ali Caglayan (Apr 04 2022 at 18:05):I am not even at Jasmin yet
Ali Caglayan (Apr 04 2022 at 18:05):I tried this in let_universe:
Ali Caglayan (Apr 04 2022 at 18:05):Section S.
Let bla@{} := Prop.
Let bli@{u} := Type@{u}.
Fail Let blo@{} := Type.
Let _@{} := Prop.
Let _@{u} := Type@{u}.
Fail Let blo@{} := Type.
End S.
this isn't nested
Ali Caglayan (Apr 04 2022 at 18:06):We fail on the second let _ since the name was given before
Ali Caglayan (Apr 04 2022 at 18:06):I can push a draft PR if you want to take a look
Ali Caglayan (Apr 04 2022 at 18:07):https://github.com/coq/coq/pull/15900
Ali Caglayan (Apr 04 2022 at 18:18):No issues when done inside a nested proof
Ali Caglayan (Apr 04 2022 at 18:19):Seems to be a section issue
Ali Caglayan (Apr 04 2022 at 18:22):But that seems to be different since the semantics of Let changes then.
Ali Caglayan (Apr 04 2022 at 18:22):Which means my patch allows somebody to do an anonymous definition using Let _ being turned into "Definition _"
Ali Caglayan (Apr 04 2022 at 18:22)::/
Gaëtan Gilbert (Apr 04 2022 at 18:22):I thought Let was some jasmin notation
Ali Caglayan (Apr 04 2022 at 18:23):No this is the vernacular Let
Ali Caglayan (Apr 04 2022 at 18:23):Unless I missed it in the Jasmin code
Gaëtan Gilbert (Apr 04 2022 at 18:23): Gaëtan Gilbert (Apr 04 2022 at 18:23):that's no vernacular
Gaëtan Gilbert (Apr 04 2022 at 18:24):vernacular Let should continue rejecting _
Ali Caglayan (Apr 04 2022 at 18:25):OK, but where is this defined then
Gaëtan Gilbert (Apr 04 2022 at 18:25):(Goal is parsed as Lemma _ so it's getting confused)
Gaëtan Gilbert (Apr 04 2022 at 18:25):don't know, run it and do Print Notation
Gaëtan Gilbert (Apr 04 2022 at 18:29): Ali Caglayan (Apr 04 2022 at 18:32):Found it
Ali Caglayan (Apr 04 2022 at 18:32):178 of utils.v
Ali Caglayan (Apr 04 2022 at 18:32):Changed ident to name everything works now
Ali Caglayan (Apr 04 2022 at 18:32):That confused me way more than it should have
Ali Caglayan (Apr 04 2022 at 18:36)::upside_down:
Pierre Roux (Apr 04 2022 at 18:54):Sorry about that, thanks a lot for the fix.
Last updated: Sep 15 2024 at 12:01 UTC