Skip to content

Commit 97cac3d

Browse files
committed
refactor(coq): simplify Bootstrap.flags
We don't use it properly in coqdoc anyway. Signed-off-by: Ali Caglayan <[email protected]>
1 parent 71dbf98 commit 97cac3d

File tree

1 file changed

+10
-16
lines changed

1 file changed

+10
-16
lines changed

src/dune_rules/coq_rules.ml

Lines changed: 10 additions & 16 deletions
Original file line numberDiff line numberDiff line change
@@ -21,13 +21,10 @@ module Bootstrap = struct
2121
(** We are compiling the prelude itself
2222
[should be replaced with (per_file ...) flags] *)
2323

24-
let flags ~coqdoc t : _ Command.Args.t =
24+
let flags t : _ Command.Args.t =
2525
match t with
2626
| No_boot -> Command.Args.empty
27-
| Bootstrap lib ->
28-
if coqdoc then
29-
S [ A "--coqlib"; Path (Path.build @@ Coq_lib.src_root lib) ]
30-
else A "-boot"
27+
| Bootstrap _ -> A "-boot"
3128
| Bootstrap_prelude -> As [ "-boot"; "-noinit" ]
3229
end
3330

@@ -100,7 +97,7 @@ let coqc_file_flags ~dir ~theories_deps ~wrapper_name ~boot_type ~ml_flags :
10097
; A wrapper_name
10198
]
10299
in
103-
[ Bootstrap.flags ~coqdoc:false boot_type; S file_flags ]
100+
[ Bootstrap.flags boot_type; S file_flags ]
104101

105102
let native_includes ~dir =
106103
let* scope = Scope.DB.find_by_dir dir in
@@ -426,16 +423,13 @@ let setup_coqdoc_rules ~sctx ~dir ~theories_deps ~wrapper_name
426423
let loc, name = (s.buildable.loc, snd s.name) in
427424
let rule =
428425
let file_flags =
429-
let file_flags =
430-
[ theories_flags ~theories_deps
431-
; A "-R"
432-
; Path (Path.build dir)
433-
; A wrapper_name
434-
]
435-
in
436-
(* BUG: we were passing No_boot before and now we have made it explicit. We
437-
probably want to do something better here. *)
438-
[ Bootstrap.flags ~coqdoc:true Bootstrap.No_boot; S file_flags ]
426+
(* BUG: We need to pass --coqlib depending on the boot_type otherwise
427+
coqdoc will not work. *)
428+
[ theories_flags ~theories_deps
429+
; A "-R"
430+
; Path (Path.build dir)
431+
; A wrapper_name
432+
]
439433
in
440434
fun mode ->
441435
let* () =

0 commit comments

Comments
 (0)