fix(coq): delay loading rules for resolving coqc #9369
Conversation
Signed-off-by: Rudi Grinberg <me@rgrinberg.com> <!-- ps-id: 76f077ec-d88b-4878-a538-c72deab5b9cd -->
rgrinberg
force-pushed
the
ps/rr/fix_coq___delay_loading_rules_for_resolving_coqc
branch
from
4e261e6
to
5bd15b3
Compare
|
This resolves the issue where the test in #7908 was hanging. We now have the more useful: Which @ejgallego and I can look into further. |
|
That one is expected. Just move the coq binary into a different directory and it will work. |
| @@ -2,6 +2,11 @@ open Import | |||
|
|
|||
| type t | |||
|
|
|||
| type origin = | |||
There was a problem hiding this comment.
Should this type be documented?
| @@ -19,4 +24,12 @@ val binary : t -> ?hint:string -> loc:Loc.t option -> string -> Action.Prog.t Me | |||
|
|
|||
| val binary_available : t -> string -> bool Memo.t | |||
| val add_binaries : t -> dir:Path.Build.t -> File_binding.Expanded.t list -> t | |||
| val create : Context.t -> local_bins:Path.Build.Set.t Memo.Lazy.t -> t | |||
|
|
|||
| val binary_with_origin | |||
There was a problem hiding this comment.
Should we add some documentation to this new API?
There was a problem hiding this comment.
Yes, I will add docs and explanations. I'm just still contemplating getting rid of the old behavior of loading binaries in the install directory everywhere. I don't remember why it's like that in the first place, so I'm digging through git history for a clue.
There was a problem hiding this comment.
Thanks a lot for the PR and for the explanation; I'm testing the patch
This comment was marked as outdated.
This comment was marked as outdated.
Sorry, something went wrong.
There was a problem hiding this comment.
I spoke too early, I had forgotten to bump the Coq lang to 0.7, indeed the problem with Coq persists, I get:
Error: Dependency cycle between:
Computing installable artifacts for package coqide-server
-> required by Computing installable artifacts for package coq-core
-> required by _build/default/coq-core.install
-> required by alias default in dune:22
and dune hangs.
| ~dir | ||
| sw) | ||
| in | ||
| Ok (Path.build (File_binding.Expanded.dst_path expanded ~dir)) |
There was a problem hiding this comment.
Why is this dst_path? Shouldn't I expand it into the source path?
cc @ejgallego
There was a problem hiding this comment.
This is just because of the initial compose with Coq patch using Super_context.resolve_program which indeed seems to resolve to the expanded path, it shouldn't matter for Coq, as we run it in such a way that is fully re-locatable (provided the deps of Coq are too, of course)
|
Replaced by #9496 |
Signed-off-by: Rudi Grinberg me@rgrinberg.com