Stream: Coq devs & plugin devs

Topic: fixing jasmin


view this post on Zulip 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.

view this post on Zulip Ali Caglayan (Apr 04 2022 at 17:00):

Ident was changed to not allow underscores

view this post on Zulip Ali Caglayan (Apr 04 2022 at 17:00):

Changing the Let to let doesn't quite workout in Jasmin however

view this post on Zulip Ali Caglayan (Apr 04 2022 at 17:01):

Should I change Let to take a name rather than an ident?

view this post on Zulip 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.

view this post on Zulip Ali Caglayan (Apr 04 2022 at 17:07):

Perhaps for the best.

view this post on Zulip 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

view this post on Zulip Ali Caglayan (Apr 04 2022 at 17:52):

I've done this but now I have an issue

view this post on Zulip Ali Caglayan (Apr 04 2022 at 17:52):

Which is name shadowing

view this post on Zulip Ali Caglayan (Apr 04 2022 at 17:52):

Unnamed_thm already exists.

view this post on Zulip Ali Caglayan (Apr 04 2022 at 17:52):

How can I freshen this name?

view this post on Zulip 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

view this post on Zulip Ali Caglayan (Apr 04 2022 at 17:57):

Am I reading this wrong or is this quite useless?

view this post on Zulip 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?

view this post on Zulip Ali Caglayan (Apr 04 2022 at 18:05):

I am not even at Jasmin yet

view this post on Zulip Ali Caglayan (Apr 04 2022 at 18:05):

I tried this in let_universe:

view this post on Zulip 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

view this post on Zulip Ali Caglayan (Apr 04 2022 at 18:06):

We fail on the second let _ since the name was given before

view this post on Zulip Ali Caglayan (Apr 04 2022 at 18:06):

I can push a draft PR if you want to take a look

view this post on Zulip Ali Caglayan (Apr 04 2022 at 18:07):

https://github.com/coq/coq/pull/15900

view this post on Zulip Ali Caglayan (Apr 04 2022 at 18:18):

No issues when done inside a nested proof

view this post on Zulip Ali Caglayan (Apr 04 2022 at 18:19):

Seems to be a section issue

view this post on Zulip Ali Caglayan (Apr 04 2022 at 18:22):

But that seems to be different since the semantics of Let changes then.

view this post on Zulip 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 _"

view this post on Zulip Ali Caglayan (Apr 04 2022 at 18:22):

:/

view this post on Zulip Gaëtan Gilbert (Apr 04 2022 at 18:22):

I thought Let was some jasmin notation

view this post on Zulip Ali Caglayan (Apr 04 2022 at 18:23):

No this is the vernacular Let

view this post on Zulip Ali Caglayan (Apr 04 2022 at 18:23):

Unless I missed it in the Jasmin code

view this post on Zulip Gaëtan Gilbert (Apr 04 2022 at 18:23):

https://gitlab.com/jasmin-lang/jasmin/-/blob/b4ace6ac0aca0895845d420ba8f7c8f80b35fa0a/proofs/lang/memory_model.v#L106

view this post on Zulip Gaëtan Gilbert (Apr 04 2022 at 18:23):

that's no vernacular

view this post on Zulip Gaëtan Gilbert (Apr 04 2022 at 18:24):

vernacular Let should continue rejecting _

view this post on Zulip Ali Caglayan (Apr 04 2022 at 18:25):

OK, but where is this defined then

view this post on Zulip Gaëtan Gilbert (Apr 04 2022 at 18:25):

(Goal is parsed as Lemma _ so it's getting confused)

view this post on Zulip Gaëtan Gilbert (Apr 04 2022 at 18:25):

don't know, run it and do Print Notation

view this post on Zulip Gaëtan Gilbert (Apr 04 2022 at 18:29):

or look into https://cs.github.com/?q=%2F%22%27Let%27%2F%20language%3Acoq%20repo%3Ajasmin-lang%2Fjasmin&scopeName=All%20repos&scope=

view this post on Zulip Ali Caglayan (Apr 04 2022 at 18:32):

Found it

view this post on Zulip Ali Caglayan (Apr 04 2022 at 18:32):

178 of utils.v

view this post on Zulip Ali Caglayan (Apr 04 2022 at 18:32):

Changed ident to name everything works now

view this post on Zulip Ali Caglayan (Apr 04 2022 at 18:32):

That confused me way more than it should have

view this post on Zulip Ali Caglayan (Apr 04 2022 at 18:36):

:upside_down:

view this post on Zulip Pierre Roux (Apr 04 2022 at 18:54):

Sorry about that, thanks a lot for the fix.


Last updated: Feb 05 2023 at 21:03 UTC