Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

[coqdoc] Fix #18516 (handling of Context) #18527

Merged
merged 1 commit into from Jan 28, 2024
Merged

[coqdoc] Fix #18516 (handling of Context) #18527

merged 1 commit into from Jan 28, 2024

Conversation

proux01
Copy link
Contributor

@proux01 proux01 commented Jan 22, 2024 •
edited by herbelin

Context was not outputting "var" definitions into the .glob file (like Variable is doing), breaking the links to section variables introduced with Context. This commit adds the missing "var" definitions, fixing the links.

Fixes #18516

  • Added / updated test-suite.
  • Added changelog.
  • Added / updated documentation.
    • Documented any new / changed user messages.
    • Updated documented syntax by running make doc_gram_rsts.
  • Opened overlay pull requests.

@coqbot-app coqbot-app bot added the needs: full CI The latest GitLab pipeline that ran was a light CI. Say "@coqbot run full ci" to get a full CI. label Jan 22, 2024
@proux01 proux01 force-pushed the hack_18516 branch 2 times, most recently from 2986241 to 0fcb61e Compare January 23, 2024 12:02
@proux01 proux01 added part: coqdoc The coqdoc binary for building documentation. kind: fix This fixes a bug or incorrect documentation. labels Jan 23, 2024
@proux01
Copy link
Contributor Author

proux01 commented Jan 23, 2024

Who is the specialist of vos nowadays? @charguer ? why on earth does adding things to the glob file break vos ?

@proux01 proux01 added the needs: changelog entry This should be documented in doc/changelog. label Jan 23, 2024
@proux01 proux01 changed the title Horrible hack to fix #18516 (refs to section variables in glob files) [coqdoc] Fix #18516 (handling of Context) Jan 23, 2024
@proux01
Copy link
Contributor Author

proux01 commented Jan 23, 2024

My bad, I just felt in the usual OCaml ; priority trap.

SkySkimmer
SkySkimmer reviewed Jan 23, 2024
View reviewed changes
vernac/vernacentries.ml Outdated Show resolved Hide resolved
@proux01 proux01 marked this pull request as ready for review January 23, 2024 15:51
@proux01 proux01 requested review from a team as code owners January 23, 2024 15:51
@proux01 proux01 mentioned this pull request Jan 23, 2024
Closed
@proux01 proux01 removed the needs: changelog entry This should be documented in doc/changelog. label Jan 23, 2024
@herbelin
Copy link
Member

herbelin commented Jan 23, 2024 •
edited

See also #13445, which greatly simplify comAssumption.ml and which implements it the same fix on the way. As you made a changelog, nice tests and documentation (which #13445 does not have) it would be good to merge this new PR first.

Note also that your choice of tags is more fine-grained than what #13445 does. #13445 relies on Constrintern.interp_named_context_evars which is not aware that the declarations are possibly going to be declared at toplevel, i.e. with an ax tag. To implement your refinement, Constrintern.interp_named_context_evars would need to get this information.

herbelin
herbelin approved these changes Jan 23, 2024
View reviewed changes
Copy link
Member

@herbelin herbelin left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Includes documentation, tests, changelog, as well as distinguishing between global/local level. Very nice.

herbelin
herbelin reviewed Jan 23, 2024
View reviewed changes
vernac/comAssumption.ml
| {CAst.v = Names.Name.Anonymous; _} -> ()
| {CAst.v = Names.Name.Name id; loc} ->
Dumpglob.dump_definition (CAst.make ?loc id) sec ty)
(List.flatten l) end;
Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Looking at it further, what is done for other declarations (in vernacentries.ml) is the following:

  • Variable/Hypothesis: "var"
  • Axiom/Parameter: "ax"
  • Definition/Theorem: "def"
  • Let: "var"

So, "def" would also be an option for LocalDef outside a section.

Copy link
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Makes sense but I'd rather keep it as "var" for now since the references (lines starting with R in the glob file) mention it as such.

Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I'm now confused. Shouldn't Context (a:=0) outside a section be considered the same as Definition a:=0 (and thus with "def") or are we rather talking about Let?

Copy link
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

You're right, I did forgot that outside-section case. Should be fixed.

Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Did you push?

Copy link
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

My bad, here it is.

interp/dumpglob.mli Outdated Show resolved Hide resolved
@proux01 proux01 added this to the 8.20+rc1 milestone Jan 25, 2024
@proux01
Copy link
Contributor Author

proux01 commented Jan 25, 2024

See also #13445, which greatly simplify comAssumption.ml

Great, while fixing this I found it sad that there is so much duplication between Variable and Context (seems to be another unfortunate leftover of the introduction of typeclasses, like all the duplication we also observe between Record and Class). I'll have a closer look at #13445 and hopefully merge it.

@herbelin would you then assign and merge this one? so that I can then rebase #13445 and I can proceed with it.

@herbelin
Copy link
Member

@herbelin would you then assign and merge this one? so that I can then rebase #13445 and I can proceed with it.

OK. Note that I already have a local rebase of the #13445 branch that I did not push yet because waiting first for #18397.

@herbelin herbelin self-assigned this Jan 25, 2024
@proux01
Fix coq#18516
9e03db1 
Context was not outputting "var" definitions int the .glob file
(like Variable is doing), breaking the links to section variables
introduced with Context. This commit adds the missing "var
"definitions, fixing the links.
@herbelin
Copy link
Member

@coqbot run full ci

@coqbot-app coqbot-app bot removed the needs: full CI The latest GitLab pipeline that ran was a light CI. Say "@coqbot run full ci" to get a full CI. label Jan 27, 2024
@herbelin
Copy link
Member

Failure of library_undecidability and http seem shared by other PRs. Nix times out.

@coqbot merge now

@coqbot-app coqbot-app bot merged commit 126398c into coq:master Jan 28, 2024
6 of 9 checks passed
@proux01 proux01 deleted the hack_18516 branch January 28, 2024 15:39
This was referenced Mar 26, 2024
Closed
Closed
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Reviewers

@herbelin herbelin herbelin approved these changes

@SkySkimmer SkySkimmer SkySkimmer left review comments

Assignees

@herbelin herbelin

Labels
kind: fix This fixes a bug or incorrect documentation. part: coqdoc The coqdoc binary for building documentation.
Projects
None yet
Milestone
8.20+rc1
Development

Successfully merging this pull request may close these issues.

Coq generates inaccurate glob information for the Context command
3 participants
@proux01 @herbelin @SkySkimmer