Stream: Coq users

Topic: Global Qed


view this post on Zulip Ralf Jung (May 20 2021 at 17:01):

Is this code deliberately accepted, or is this a bug?

Lemma test: True.
Proof.
exact I.
Global Qed.

view this post on Zulip Michael Soegtrop (May 20 2021 at 19:45):

It is documented that Lemma & Co can take local and with that also global attributes. Since Qed is the command which actually saves the lemma in the environment, it is not that inconsequential, that it takes local and global attributes as well. The saving of the lemma in the environment can be changed at the point of Qed in other ways, say the name with Save. If one can change the name at this point, why not also the global/local?

view this post on Zulip Gaëtan Gilbert (May 20 2021 at 19:52):

it's bugged, it just ignores the attribute

Lemma foo : Prop.
Proof.
  exact True.
#[potato] Qed.

is also accepted...

view this post on Zulip Théo Zimmermann (May 20 2021 at 19:52):

But does Local Qed actually works and do anything? It sure isn't documented, so it is at least a documentation issue.

view this post on Zulip Enrico Tassi (May 20 2021 at 20:03):

I think we should give an error.

view this post on Zulip Emilio Jesús Gallego Arias (May 20 2021 at 20:52):

Théo Zimmermann said:

But does Local Qed actually works and do anything? It sure isn't documented, so it is at least a documentation issue.

As noted by Gaëtan it does nothing:

view this post on Zulip Emilio Jesús Gallego Arias (May 20 2021 at 20:53):

  | VernacEndProof pe ->
    VtCloseProof (vernac_end_proof pe)

view this post on Zulip Emilio Jesús Gallego Arias (May 20 2021 at 20:53):

let vernac_end_proof ~lemma ~pm = let open Vernacexpr in function
  | Admitted ->
    Declare.Proof.save_admitted ~pm ~proof:lemma
  | Proved (opaque,idopt) ->
    let pm, _ = Declare.Proof.save ~pm ~proof:lemma ~opaque ~idopt
    in pm

and indeed there is little support for doing anything else.

view this post on Zulip Théo Zimmermann (May 21 2021 at 10:02):

Emilio Jesús Gallego Arias said:

Théo Zimmermann said:

But does Local Qed actually works and do anything? It sure isn't documented, so it is at least a documentation issue.

As noted by Gaëtan it does nothing:

Indeed, I was answering to Michael. Note that our messages were posted at the same time.

view this post on Zulip Ralf Jung (May 21 2021 at 17:35):

All right, opened a bug: https://github.com/coq/coq/issues/14360


Last updated: Feb 04 2023 at 22:29 UTC