Skip to content

Fix roots in solution2evd - #614

Open
Tragicus wants to merge 1 commit into
LPCIC:masterfrom
Tragicus:fix-roots-solution2evd
Open

Fix roots in solution2evd#614
Tragicus wants to merge 1 commit into
LPCIC:masterfrom
Tragicus:fix-roots-solution2evd

Conversation

@Tragicus

@Tragicus Tragicus commented Mar 19, 2024

Copy link
Copy Markdown
Contributor

It may happen that coq-elpi aliases something in the input evar_map and then drops the alias because it does not appear in the solution returned by coq-elpi. However, this alias might be referenced in the evar_map, so it should not be dropped. This PR fixes the issue by adding the evars from the input evar_map to the roots of the computation of reachable evars.
This relies on some API from coq that does not exist yet.

@CohenCyril

Copy link
Copy Markdown
Collaborator

@Tragicus could you link to a branch of Coq which exposes the primitive you needed?

@Tragicus

Copy link
Copy Markdown
Contributor Author

Yes, here it is (I only need the contents of engine/evd.ml): https://github.com/Tragicus/coq/tree/utils
For reference, I opened a PR for this branch: rocq-prover/rocq#18820

@gares

gares commented Mar 20, 2024

Copy link
Copy Markdown
Contributor

I think the old code was actually implementing Evd.undefined_evars, about the other one I don't know.

@gares
gares force-pushed the fix-roots-solution2evd branch from 63fa6d8 to e9375f3 Compare June 27, 2024 08:58
@gares
gares force-pushed the fix-roots-solution2evd branch from e9375f3 to 7c7ccfa Compare June 27, 2024 09:18
@gares

gares commented Jun 28, 2024

Copy link
Copy Markdown
Contributor

@Tragicus can you tell me if this code does what you wanted?

Then we definitely need to do some benchmarking

@Tragicus

Copy link
Copy Markdown
Contributor Author

It was long ago so I might be mistaken, but I am pretty sure this solved our issue back then. I can do the benchmarking tomorrow.

@Tragicus

Copy link
Copy Markdown
Contributor Author

I can compile neither master nor coq-master neither on coq's master nor v8.19. Can you tell me which branches I should take?

@gares

gares commented Jun 30, 2024

Copy link
Copy Markdown
Contributor

Maybe you need to rebade this pr, but currently master works with 8.19, 8.20rc1 and master, both with opam and Nix.

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

3 participants