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

[add-const] do not recompute the uctx for the evar map #651

Merged
merged 1 commit into from
Jul 17, 2024
Merged

[add-const] do not recompute the uctx for the evar map #651

merged 1 commit into from
Jul 17, 2024

Conversation

gares
Copy link
Contributor

@gares gares commented Jul 4, 2024 •
edited by SkySkimmer
Loading

@gares
Copy link
Contributor Author

gares commented Jul 4, 2024

CC @ppedrot

@gares gares force-pushed the master-of-the-universes branch 5 times, most recently from 0c8466a to 9823c22 Compare July 8, 2024 12:48
@gares
Copy link
Contributor Author

gares commented Jul 8, 2024

Hello, I need help in order to remove the use of the non-sound API.
I'm getting this:

Debug: elpi lets escape exception: Conversion test raised an anomaly:
Anomaly
"in Univ.repr: Universe elpi.apps.locker.tests.test_locker.93 undefined."
Please report at http://coq.inria.fr/bugs/.
File "./apps/locker/tests/test_locker.v", line 95, characters 0-79:
Error: Conversion test raised an anomaly:
Anomaly
"in Univ.repr: Universe elpi.apps.locker.tests.test_locker.93 undefined."
Please report at http://coq.inria.fr/bugs/.
Raised at Exninfo.iraise in file "clib/exninfo.ml", line 79, characters 4-11
Called from AcyclicGraph.Make.enforce_lt in file "lib/acyclicGraph.ml", line 670, characters 15-28
Called from UGraph.enforce_constraint0 in file "kernel/uGraph.ml", line 94, characters 38-68
Called from UGraph.enforce_constraint in file "kernel/uGraph.ml", line 100, characters 37-62
Called from Stdlib__Set.Make.fold in file "set.ml", line 383, characters 34-55
Called from UState.merge_constraints in file "engine/uState.ml", line 286, characters 6-38
Called from UState.add_universe_constraints in file "engine/uState.ml", line 714, characters 16-60
Called from Evd.add_universe_constraints in file "engine/evd.ml", line 962, characters 23-68
Called from Reductionops.infer_conv_gen in file "pretyping/reductionops.ml", line 1320, characters 17-58
Re-raised at Exninfo.iraise in file "clib/exninfo.ml", line 81, characters 4-38
Called from Evarconv.infer_conv_noticing_evars in file "pretyping/evarconv.ml", line 629, characters 8-70
Called from Evarconv.evar_conv_x in file "pretyping/evarconv.ml", line 646, characters 6-80
Called from Evarconv.unify_leq_delay in file "pretyping/evarconv.ml", line 1959, characters 8-45
Called from Typing.judge_of_apply.apply_rec in file "pretyping/typing.ml", line 105, characters 10-58
Called from Typing.type_of in file "pretyping/typing.ml", line 646, characters 17-36

that comes from

mlock #[universes(polymorphic)] Definition id2@{u} (T : Type@{u}) (x : T) := x.

Note that f4340e1 works if you run dune build apps/locker/tests/test_locker.vo

@gares
Copy link
Contributor Author

gares commented Jul 8, 2024

The message above is for @SkySkimmer and @ppedrot

SkySkimmer
SkySkimmer reviewed Jul 8, 2024
View reviewed changes
src/coq_elpi_builtins.ml Outdated
let declare_definition _ using ~cinfo ~info ~opaque ~body sigma =
let using = Option.map Proof_using.using_from_string using in
let gr, uctx = Declare.declare_definition_full ~cinfo ~info ~opaque ~body ?using sigma in
gr, UState.context_set uctx
Copy link
Collaborator

Choose a reason for hiding this comment

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

maybe need to do if poly then empty else UState.context_set uctx (not sure where poly is, I think either cinfo or info)

SkySkimmer
SkySkimmer reviewed Jul 8, 2024
View reviewed changes
src/coq_elpi_HOAS.ml Outdated
UState.demote_global_univs env uctx
[%%else]
let demote uctx sigma0 env =
UState.demote_global_univs_sound uctx (Evd.evar_universe_context sigma0)
Copy link
Collaborator

Choose a reason for hiding this comment

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

Might be useful to add a debug print like "demoting (print uctx)"

@gares gares force-pushed the master-of-the-universes branch 3 times, most recently from 0a3c5df to bac1c4f Compare July 14, 2024 15:28
gares
gares commented Jul 14, 2024
View reviewed changes
.nix/config.nix Outdated
@@ -32,7 +32,13 @@
reglang.job = false;
};

"coq-master".ocamlPackages = {
Copy link
Contributor Author

Choose a reason for hiding this comment

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

remove before merge

@gares gares force-pushed the master-of-the-universes branch from bac1c4f to 414b24e Compare July 15, 2024 06:17
@SkySkimmer SkySkimmer mentioned this pull request Jul 15, 2024
Merged
@gares gares force-pushed the master-of-the-universes branch 2 times, most recently from 1afd417 to 8de3026 Compare July 15, 2024 16:27
@gares gares marked this pull request as ready for review July 15, 2024 16:28
@gares gares force-pushed the master-of-the-universes branch from 8de3026 to 544bff1 Compare July 15, 2024 19:40
SkySkimmer
SkySkimmer reviewed Jul 15, 2024
View reviewed changes
src/coq_elpi_builtins.ml
Comment on lines -537 to +546
let global_univs = UGraph.domain (Environ.universes (Global.env ())) in
let env = Global.env () in
let is_global u =
match Univ.Universe.level u with
| None -> true
| Some l -> Univ.Level.Set.mem l global_univs in
| Some l -> is_global_level env l in
Copy link
Collaborator

Choose a reason for hiding this comment

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

you could merge this in master separately btw

Copy link
Contributor Author

Choose a reason for hiding this comment

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

right, but I hope to merge this soon, keeping the PR going is draining too much of my time

@ppedrot
Copy link
Collaborator

ppedrot commented Jul 17, 2024

Please merge now

@gares gares merged commit 507f037 into master Jul 17, 2024
44 checks passed
@gares gares deleted the master-of-the-universes branch July 17, 2024 11:32
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Reviewers

@SkySkimmer SkySkimmer SkySkimmer left review comments

Assignees
No one assigned
Labels
None yet
Projects
None yet
Milestone
No milestone
Development

Successfully merging this pull request may close these issues.
3 participants
@gares @ppedrot @SkySkimmer