Emilio Jesús Gallego Arias (Jun 11 2022 at 10:31): Emilio Jesús Gallego Arias (Jun 11 2022 at 10:31):@Ali Caglayan , I was looking at why -boot is not passed to coqdoc, but I'm puzzled, it seems the code should pass it, right?
Emilio Jesús Gallego Arias (Jun 11 2022 at 10:31):coqdoc_file_flags tries to do it
Emilio Jesús Gallego Arias (Jun 11 2022 at 10:31):it is a laziness bug?
Ali Caglayan (Jun 11 2022 at 10:32):I'm not sure, have you gotten coqdoc to work with boot before?
Ali Caglayan (Jun 11 2022 at 10:32):Oh wait I filter that flag
Emilio Jesús Gallego Arias (Jun 11 2022 at 10:32):yes it works if I pass the correct flags manuall
Ali Caglayan (Jun 11 2022 at 10:32):coqdoc flags are filtered because it errors on the boot flag
Ali Caglayan (Jun 11 2022 at 10:33):There should be a coqdoc_flags somewhere
Ali Caglayan (Jun 11 2022 at 10:34): let coqdoc_file_flags cctx =
let file_flags =
[ theories_flags cctx
; Command.Args.A "-R"
; Path (Path.build cctx.dir)
; A cctx.wrapper_name
]
in
[ Command.Args.Dyn
(Resolve.Memo.map
~f:(fun b -> Command.Args.S (Bootstrap.flags b))
cctx.boot_type
|> Resolve.Memo.read)
; S file_flags
]
I don't see the filter
Emilio Jesús Gallego Arias (Jun 11 2022 at 10:34):Tho I think we need to do a bit of refactoring
Ali Caglayan (Jun 11 2022 at 10:35):thats true, but now that composition has been merged that should be easier
Emilio Jesús Gallego Arias (Jun 11 2022 at 10:35):I propose this for now:
Coq_libBootstrap.flags take care of it Emilio Jesús Gallego Arias (Jun 11 2022 at 10:35):Yeah, but why is the flag not sent to coqdoc?
Emilio Jesús Gallego Arias (Jun 11 2022 at 10:35):It should
Ali Caglayan (Jun 11 2022 at 10:35):Are you sure?
Ali Caglayan (Jun 11 2022 at 10:35):Can you check the actual command
Ali Caglayan (Jun 11 2022 at 10:36):I'm totally not sure
Emilio Jesús Gallego Arias (Jun 11 2022 at 10:36):(cd _build/.sandbox/85f33dd7434aaa82f2761c47dadf4433/default/finmap && ../../install/default/bin/coqdoc -R ../coq-master/theories Coq -Q ../math-comp/mathcomp/ssreflect mathcomp.ssreflect -R . mathcomp.finmap --toc --html -d mathcomp.finmap.html finmap.v multiset.v set.v)
This resolve stuff is really brittle sometimes
Emilio Jesús Gallego Arias (Jun 11 2022 at 10:37):can be very hard to reason about, as it happened with the bug in (env (coq ...))
Ali Caglayan (Jun 11 2022 at 10:38):Wait
Ali Caglayan (Jun 11 2022 at 10:38):theories_flags doesn't have boot does it?
Emilio Jesús Gallego Arias (Jun 11 2022 at 10:39):We add -R Coq $path_to_coqlib to theories flag in coq_lib
Ali Caglayan (Jun 11 2022 at 10:39): let theories_flags =
let setup_theory_flag lib =
let dir = Coq_lib.src_root lib in
let binding_flag = if Coq_lib.implicit lib then "-R" else "-Q" in
[ Command.Args.A binding_flag
; Path (Path.build dir)
; A (Coq_lib.name lib |> Coq_lib_name.wrapper)
]
in
fun t ->
Resolve.Memo.args
(let open Resolve.Memo.O in
let+ libs = t.theories_deps in
Command.Args.S (List.concat_map libs ~f:setup_theory_flag))
I suggest we move this to Bootstrap.flags
Emilio Jesús Gallego Arias (Jun 11 2022 at 10:39):This is the code I suggest to remove:
Emilio Jesús Gallego Arias (Jun 11 2022 at 10:40): let theories =
let open Resolve.O in
let* boot = boot in
match boot with
| None -> theories
| Some boot ->
let+ theories = theories in
(* TODO: if lib is boot, don't add boot dep *)
(* maybe use the loc for boot? *)
(Loc.none, boot) :: theories
ah wait I see the problem
Ali Caglayan (Jun 11 2022 at 10:40): let coqdoc_file_flags cctx =
let file_flags =
[ theories_flags cctx
; Command.Args.A "-R"
; Path (Path.build cctx.dir)
; A cctx.wrapper_name
]
in
[ Command.Args.Dyn
(Resolve.Memo.map
~f:(fun b -> Command.Args.S (Bootstrap.flags b))
cctx.boot_type
|> Resolve.Memo.read)
; S file_flags
]
mathcomp is not a boot lib so -boot wasn't being passed
Ali Caglayan (Jun 11 2022 at 10:41):right? Or am I misinterpreting
Emilio Jesús Gallego Arias (Jun 11 2022 at 10:41):The code in coqc_file_flags is identical and it gets boot
Ali Caglayan (Jun 11 2022 at 10:41):Since it is composed with a boot lib, it should pass -boot everywhere
Emilio Jesús Gallego Arias (Jun 11 2022 at 10:41):Yes, I think so
Emilio Jesús Gallego Arias (Jun 11 2022 at 10:42):Recall that actually composition was implemented since coq lang 0.2
Emilio Jesús Gallego Arias (Jun 11 2022 at 10:43):what was missing what the public_theories DB
Emilio Jesús Gallego Arias (Jun 11 2022 at 10:43):so in this sense, the flags should include boot, but I think resolve is messing with our lives here...
Ali Caglayan (Jun 11 2022 at 10:46):I don't understand why you think Resolve it causing issues here
Ali Caglayan (Jun 11 2022 at 10:46):The composition Coq_lib.DB is a rewrite from 0.2 composition
Emilio Jesús Gallego Arias (Jun 11 2022 at 10:47):Ali Caglayan said:
I don't understand why you think Resolve it causing issues here
It is a hypothesis
Emilio Jesús Gallego Arias (Jun 11 2022 at 10:47):what's your explanantion for -boot not appearing?
Ali Caglayan (Jun 11 2022 at 10:49):I'm having a look
Emilio Jesús Gallego Arias (Jun 11 2022 at 10:53):Maybe this is the culprit?
Emilio Jesús Gallego Arias (Jun 11 2022 at 10:53): let rule =
let file_flags = Context.coqdoc_file_flags cctx in
fun mode ->
let* () =
nope, false flag
Ali Caglayan (Jun 11 2022 at 12:11):I'm confused
Ali Caglayan (Jun 11 2022 at 12:11):I did a test, and -boot seems to be passed
Emilio Jesús Gallego Arias (Jun 11 2022 at 12:28):Can you give me a dune build $target that shows it in current Coq universe main?
Ali Caglayan (Jun 11 2022 at 12:42):No sorry I read it wrong
Ali Caglayan (Jun 11 2022 at 12:42):You're correct it is not being passed
Ali Caglayan (Jun 11 2022 at 12:43):I was looking at the output of --verbose
Last updated: Jun 03 2023 at 17:29 UTC