-
Notifications
You must be signed in to change notification settings - Fork 416
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.
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(coq): delay loading rules for resolving coqc #9369
Changes from all commits
File filter
Filter by extension
Conversations
Jump to
Diff view
Diff view
There are no files selected for viewing
Original file line number | Diff line number | Diff line change |
---|---|---|
|
@@ -2,6 +2,11 @@ open Import | |
|
||
type t | ||
|
||
type origin = | ||
{ binding : File_binding.Unexpanded.t | ||
; dir : Path.Build.t | ||
} | ||
|
||
(** Force the computation of the internal list of binaries. This is exposed as | ||
some error checking is only performed during this computation and some | ||
errors will go unreported unless this computation takes place. *) | ||
|
@@ -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. Choose a reason for hiding this commentThe reason will be displayed to describe this comment to others. Learn more. Should we add some documentation to this new API? There was a problem hiding this comment. Choose a reason for hiding this commentThe reason will be displayed to describe this comment to others. Learn more. 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. Choose a reason for hiding this commentThe reason will be displayed to describe this comment to others. Learn more. Thanks a lot for the PR and for the explanation; I'm testing the patch
This comment was marked as outdated.
Sorry, something went wrong. There was a problem hiding this comment. Choose a reason for hiding this commentThe reason will be displayed to describe this comment to others. Learn more. I spoke too early, I had forgotten to bump the Coq lang to 0.7, indeed the problem with Coq persists, I get:
and dune hangs. |
||
: t | ||
-> ?hint:string | ||
-> loc:Loc.t option | ||
-> Filename.t | ||
-> ([ `External of Path.t | `Origin of origin ], Action.Prog.Not_found.t) result Memo.t | ||
|
||
val create : Context.t -> local_bins:origin Path.Build.Map.t Memo.Lazy.t -> t |
Original file line number | Diff line number | Diff line change |
---|---|---|
|
@@ -92,12 +92,20 @@ end = struct | |
end | ||
|
||
let coqc ~loc ~dir ~sctx = | ||
Super_context.resolve_program_memo | ||
sctx | ||
"coqc" | ||
~dir | ||
~loc:(Some loc) | ||
~hint:"opam install coq" | ||
let* artifacts = Super_context.env_node sctx ~dir >>= Env_node.artifacts in | ||
Artifacts.binary_with_origin artifacts ~loc:(Some loc) ~hint:"opam install coq" "coqc" | ||
>>= function | ||
| Error e -> Memo.return @@ Error e | ||
| Ok (`External p) -> Memo.return @@ Ok p | ||
| Ok (`Origin { Artifacts.binding; dir }) -> | ||
let+ expanded = | ||
File_binding.Unexpanded.expand binding ~dir ~f:(fun sw -> | ||
Expander.With_reduced_var_set.expand_str | ||
~context:(Super_context.context sctx) | ||
~dir | ||
sw) | ||
in | ||
Ok (Path.build (File_binding.Expanded.dst_path expanded ~dir)) | ||
There was a problem hiding this comment. Choose a reason for hiding this commentThe reason will be displayed to describe this comment to others. Learn more. Why is this cc @ejgallego There was a problem hiding this comment. Choose a reason for hiding this commentThe reason will be displayed to describe this comment to others. Learn more. This is just because of the initial compose with Coq patch using |
||
;; | ||
|
||
let select_native_mode ~sctx ~dir (buildable : Coq_stanza.Buildable.t) = | ||
|
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Should this type be documented?