-
Notifications
You must be signed in to change notification settings - Fork 413
Commit
This commit does not belong to any branch on this repository, and may belong to a fork outside of the repository.
refactor: declare directory targets without loading rules (#9149)
Signed-off-by: Rudi Grinberg <[email protected]>
- Loading branch information
Showing
9 changed files
with
110 additions
and
113 deletions.
There are no files selected for viewing
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,27 @@ | ||
open Import | ||
open Memo.O | ||
|
||
let coqdoc_directory ~mode ~obj_dir ~name = | ||
Path.Build.relative | ||
obj_dir | ||
(Coq_lib_name.to_string name | ||
^ | ||
match mode with | ||
| `Html -> ".html" | ||
| `Latex -> ".tex") | ||
;; | ||
|
||
let coqdoc_directory_targets ~dir:obj_dir (theory : Coq_stanza.Theory.t) = | ||
let+ (_ : Coq_lib.DB.t) = | ||
(* We force the creation of the coq_lib db here so that errors there can | ||
appear before any errors to do with directory targets from coqdoc. *) | ||
let* scope = Scope.DB.find_by_dir obj_dir in | ||
Scope.coq_libs scope | ||
in | ||
let loc = theory.buildable.loc in | ||
let name = snd theory.name in | ||
Path.Build.Map.of_list_exn | ||
[ coqdoc_directory ~mode:`Html ~obj_dir ~name, loc | ||
; coqdoc_directory ~mode:`Latex ~obj_dir ~name, loc | ||
] | ||
;; |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,15 @@ | ||
open Import | ||
|
||
(* This code lives in its own module so that it's usable in [Dir_status] | ||
without creating dependency cycles *) | ||
|
||
val coqdoc_directory | ||
: mode:[< `Html | `Latex ] | ||
-> obj_dir:Path.Build.t | ||
-> name:Coq_lib_name.t | ||
-> Path.Build.t | ||
|
||
val coqdoc_directory_targets | ||
: dir:Path.Build.t | ||
-> Coq_stanza.Theory.t | ||
-> Loc.t Path.Build.Map.t Memo.t |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters