Stream: Dune devs & users

Topic: coqdoc and boot build


view this post on Zulip 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?

view this post on Zulip Emilio Jesús Gallego Arias (Jun 11 2022 at 10:31):

coqdoc_file_flags tries to do it

view this post on Zulip Emilio Jesús Gallego Arias (Jun 11 2022 at 10:31):

it is a laziness bug?

view this post on Zulip Ali Caglayan (Jun 11 2022 at 10:32):

I'm not sure, have you gotten coqdoc to work with boot before?

view this post on Zulip Ali Caglayan (Jun 11 2022 at 10:32):

Oh wait I filter that flag

view this post on Zulip Emilio Jesús Gallego Arias (Jun 11 2022 at 10:32):

yes it works if I pass the correct flags manuall

view this post on Zulip Ali Caglayan (Jun 11 2022 at 10:32):

coqdoc flags are filtered because it errors on the boot flag

view this post on Zulip Ali Caglayan (Jun 11 2022 at 10:33):

There should be a coqdoc_flags somewhere

view this post on Zulip 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
    ]

view this post on Zulip Emilio Jesús Gallego Arias (Jun 11 2022 at 10:34):

I don't see the filter

view this post on Zulip Emilio Jesús Gallego Arias (Jun 11 2022 at 10:34):

Tho I think we need to do a bit of refactoring

view this post on Zulip Ali Caglayan (Jun 11 2022 at 10:35):

thats true, but now that composition has been merged that should be easier

view this post on Zulip Emilio Jesús Gallego Arias (Jun 11 2022 at 10:35):

I propose this for now:

view this post on Zulip Emilio Jesús Gallego Arias (Jun 11 2022 at 10:35):

Yeah, but why is the flag not sent to coqdoc?

view this post on Zulip Emilio Jesús Gallego Arias (Jun 11 2022 at 10:35):

It should

view this post on Zulip Ali Caglayan (Jun 11 2022 at 10:35):

Are you sure?

view this post on Zulip Ali Caglayan (Jun 11 2022 at 10:35):

Can you check the actual command

view this post on Zulip Ali Caglayan (Jun 11 2022 at 10:36):

I'm totally not sure

view this post on Zulip 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)

view this post on Zulip Emilio Jesús Gallego Arias (Jun 11 2022 at 10:37):

This resolve stuff is really brittle sometimes

view this post on Zulip 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 ...))

view this post on Zulip Ali Caglayan (Jun 11 2022 at 10:38):

Wait

view this post on Zulip Ali Caglayan (Jun 11 2022 at 10:38):

theories_flags doesn't have boot does it?

view this post on Zulip Emilio Jesús Gallego Arias (Jun 11 2022 at 10:39):

We add -R Coq $path_to_coqlib to theories flag in coq_lib

view this post on Zulip 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))

view this post on Zulip Emilio Jesús Gallego Arias (Jun 11 2022 at 10:39):

I suggest we move this to Bootstrap.flags

view this post on Zulip Emilio Jesús Gallego Arias (Jun 11 2022 at 10:39):

This is the code I suggest to remove:

view this post on Zulip 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

view this post on Zulip Ali Caglayan (Jun 11 2022 at 10:40):

ah wait I see the problem

view this post on Zulip 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
    ]

view this post on Zulip Ali Caglayan (Jun 11 2022 at 10:40):

mathcomp is not a boot lib so -boot wasn't being passed

view this post on Zulip Ali Caglayan (Jun 11 2022 at 10:41):

right? Or am I misinterpreting

view this post on Zulip Emilio Jesús Gallego Arias (Jun 11 2022 at 10:41):

The code in coqc_file_flags is identical and it gets boot

view this post on Zulip Ali Caglayan (Jun 11 2022 at 10:41):

Since it is composed with a boot lib, it should pass -boot everywhere

view this post on Zulip Emilio Jesús Gallego Arias (Jun 11 2022 at 10:41):

Yes, I think so

view this post on Zulip Emilio Jesús Gallego Arias (Jun 11 2022 at 10:42):

Recall that actually composition was implemented since coq lang 0.2

view this post on Zulip Emilio Jesús Gallego Arias (Jun 11 2022 at 10:43):

what was missing what the public_theories DB

view this post on Zulip 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...

view this post on Zulip Ali Caglayan (Jun 11 2022 at 10:46):

I don't understand why you think Resolve it causing issues here

view this post on Zulip Ali Caglayan (Jun 11 2022 at 10:46):

The composition Coq_lib.DB is a rewrite from 0.2 composition

view this post on Zulip 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

view this post on Zulip Emilio Jesús Gallego Arias (Jun 11 2022 at 10:47):

what's your explanantion for -boot not appearing?

view this post on Zulip Ali Caglayan (Jun 11 2022 at 10:49):

I'm having a look

view this post on Zulip Emilio Jesús Gallego Arias (Jun 11 2022 at 10:53):

Maybe this is the culprit?

view this post on Zulip 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* () =

view this post on Zulip Emilio Jesús Gallego Arias (Jun 11 2022 at 10:54):

nope, false flag

view this post on Zulip Ali Caglayan (Jun 11 2022 at 12:11):

I'm confused

view this post on Zulip Ali Caglayan (Jun 11 2022 at 12:11):

I did a test, and -boot seems to be passed

view this post on Zulip 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?

view this post on Zulip Ali Caglayan (Jun 11 2022 at 12:42):

No sorry I read it wrong

view this post on Zulip Ali Caglayan (Jun 11 2022 at 12:42):

You're correct it is not being passed

view this post on Zulip Ali Caglayan (Jun 11 2022 at 12:43):

I was looking at the output of --verbose


Last updated: Jan 30 2023 at 18:04 UTC