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

fix sigma pruning when calling ltac, reachability is not correct #581

Merged
merged 2 commits into from
Jan 29, 2024
Merged

fix sigma pruning when calling ltac, reachability is not correct #581

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
2 commits
Select commit Hold shift + click to select a range
6b758c5
fix sigma pruning when calling ltac, reachability is not correct
gares Jan 26, 2024
849a95d
fix reachability test
gares Jan 26, 2024
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
4 changes: 3 additions & 1 deletion coq-builtin-synterp.elpi
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -306,10 +306,12 @@ external pred coq.env.current-section-path o:list string.
kind clause type.
type clause id -> grafting -> prop -> clause.

% Specify if the clause has to be grafted before or after a named clause
% Specify if the clause has to be grafted before, grafted after or replace
% a named clause
kind grafting type.
type before id -> grafting.
type after id -> grafting.
type replace id -> grafting.

% Specify to which module the clause should be attached to
kind scope type.
Expand Down
4 changes: 3 additions & 1 deletion coq-builtin.elpi
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -1711,10 +1711,12 @@ external pred coq.extra-dep i:id, o:option id.
kind clause type.
type clause id -> grafting -> prop -> clause.

% Specify if the clause has to be grafted before or after a named clause
% Specify if the clause has to be grafted before, grafted after or replace
% a named clause
kind grafting type.
type before id -> grafting.
type after id -> grafting.
type replace id -> grafting.

% Specify to which module the clause should be attached to
kind scope type.
Expand Down
2 changes: 1 addition & 1 deletion examples/example_abs_evars.v
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -88,7 +88,7 @@ solve (goal _ _ _ _ [trm T] as G) GL :-
solve (goal _ _ T _ [] as G) GL :-
std.assert! (abs-evars T ClosedT N) "closure fails",
coq.mk-app {{ (fun x : lp:ClosedT => x) _ }} {coq.mk-n-holes N} R,
refine R G GL.
refine R G GL.

}}.
Elpi Typecheck.
Expand Down
12 changes: 8 additions & 4 deletions src/coq_elpi_HOAS.ml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -2411,7 +2411,10 @@ let get_declared_goals all_goals constraints state assignments pp_ctx =

let rec reachable1 sigma root acc =
let EvarInfo info = Evd.find sigma root in
let res = match Evd.evar_body info with Evd.Evar_empty -> Evar.Set.add root acc | Evd.Evar_defined _ -> acc in
let res =
match Evd.evar_body info with
| Evd.Evar_empty -> Evar.Set.add root acc
| Evd.Evar_defined d -> acc in
let res = Evar.Set.union res @@ Evarutil.filtered_undefined_evars_of_evar_info sigma info in
if Evar.Set.equal res acc then acc else reachable sigma res res
and reachable sigma roots acc =
Expand All @@ -2429,13 +2432,14 @@ let reachable sigma roots acc =
let solution2evd sigma0 { API.Data.constraints; assignments; state; pp_ctx } roots =
let state, solved_goals, _, _gls = elpi_solution_to_coq_solution ~calldepth:0 constraints state in
let sigma = get_sigma state in
let all_goals = reachable sigma roots Evar.Set.empty in
let roots = Evd.fold_undefined (fun k _ acc -> Evar.Set.add k acc) sigma0 roots in
let reachable_undefined_evars = reachable sigma roots Evar.Set.empty in
let declared_goals, shelved_goals =
get_declared_goals (Evar.Set.diff all_goals solved_goals) constraints state assignments pp_ctx in
get_declared_goals (Evar.Set.diff reachable_undefined_evars solved_goals) constraints state assignments pp_ctx in
debug Pp.(fun () -> str "Goals: " ++ prlist_with_sep spc Evar.print declared_goals);
debug Pp.(fun () -> str "Shelved Goals: " ++ prlist_with_sep spc Evar.print shelved_goals);
Evd.fold_undefined (fun k _ sigma ->
if Evar.Set.mem k all_goals || Evd.mem sigma0 k then sigma
if Evar.Set.mem k reachable_undefined_evars then sigma
else Evd.remove sigma k
Copy link
Collaborator

Choose a reason for hiding this comment

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

Sorry for hijacking this PR, but you definitely shouldn't reimplement your own pruning in a plugin. As a matter of fact, I wonder why Evd.remove is not marked as deprecated in the Coq API as you can easily wreak havoc (and definitely will if people use additional Store primitives in an evarmap).

We should instead provide a pruning function directly with Evd and ask in the API when creating user-defined evar data to provide functions explaining how the new data creates pointers to other blocks. It is more than time to realize that an evarmap is a proper heap...

Copy link
Contributor Author

Choose a reason for hiding this comment

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

I'm all for a heap that comes with a garbage collector, but currently it does not.
Worse, there is code that insists all your allocations are pointed to by the root, that is, that you don't leave garbage.

I'm happy to use any API you provide.

After this is merged, we can see if it also fixes the other bug affecting the TC solver.

) sigma sigma,
declared_goals,
Expand Down
Loading