Adding support for a "dune coq top" command

CHANGES.md

@@ -1,6 +1,8 @@
 3.1.0 (Unreleased)
 ------------------
 
+- Add `dune coq top` command for running a Coq toplevel (#5457, @rlepigre)
+
 - Fix dune exec dumping database in wrong directory (#5544, @bobot)
 
 - Always output absolute paths for locations in RPC reported diagnostics

bin/coq.ml

@@ -0,0 +1,21 @@
+open Import
+
+let doc =
+  "Command group related to Coq."
+
+let sub_commands_synopsis =
+  Common.command_synopsis
+    [ "coq top FILE -- ARGS"
+    ]
+
+let man =
+  [ `Blocks sub_commands_synopsis
+  ]
+
+let info = Term.info ~doc ~man "coq"
+
+let group =
+  ( Term.Group.Group
+      [ in_group Coqtop.command
+      ]
+  , info )

bin/coq.mli

@@ -0,0 +1,3 @@
+open Import
+
+val group : unit Term.Group.t

bin/coqtop.ml

@@ -0,0 +1,128 @@
+open Stdune
+open Import
+
+let doc =
+  "Execute the Coq toplevel with the local configuration."
+
+let man =
+  [ `S "DESCRIPTION"
+  ; `P
+      {|$(b,dune coq top FILE -- ARGS) runs the Coq toplevel to process the
+          given $(b,FILE). The given arguments are completed according to the
+          local configuration. This is equivalent to running $(b,coqtop ARGS)
+          with a $(b,_CoqProject) file containing the local configurations
+          from the $(b,dune) files, but does not require maintaining a
+          $(b,_CoqProject) file.|}
+  ; `Blocks Common.help_secs
+  ]
+
+let info = Term.info "top" ~doc ~man
+
+let term =
+  let+ common = Common.term
+  and+ context =
+    Common.context_arg ~doc:{|Run the Coq toplevel in this build context.|}
+  and+ coqtop =
+    let doc = "Run the given toplevel command instead of the default." in
+    Arg.(value & opt string "coqtop" & info [ "toplevel" ] ~docv:"CMD" ~doc)
+  and+ coq_file_arg =
+    Arg.(required & pos 0 (some string) None (Arg.info [] ~docv:"COQFILE"))
+  and+ extra_args =
+    Arg.(value & pos_right 0 string [] (Arg.info [] ~docv:"ARGS"))
+  in
+  let config = Common.init common in
+  let coqtop, argv, env =
+    Scheduler.go ~common ~config (fun () ->
+        let open Fiber.O in
+        let* setup = Import.Main.setup () in
+        let* setup = Memo.Build.run setup in
+        let sctx = Import.Main.find_scontext_exn setup ~name:context in
+        let context = Dune_rules.Super_context.context sctx in
+        (* Try to compute a relative path if we got an absolute path. *)
+        let coq_file_arg =
+          let cwd = Path.external_ (Path.External.initial_cwd) in
+          let file =
+            (* Best-effort symbolic link unfolding. *)
+            let file = Fpath.follow_symlinks coq_file_arg in
+            Option.value file ~default:coq_file_arg
+          in
+          let file = Path.of_filename_relative_to_initial_cwd file in
+          let cwd = Path.to_string cwd in
+          let file = Path.to_string file in
+          match String.drop_prefix ~prefix:(cwd ^ "/") file with
+          | None -> coq_file_arg
+          | Some s -> s
+        in
+        let coq_file_build =
+          let p = Common.prefix_target common coq_file_arg in
+          Path.Build.relative context.build_dir p
+        in
+        let dir =
+          let dir = Filename.dirname coq_file_arg in
+          let p = Common.prefix_target common dir in
+          Path.Build.relative context.build_dir p
+        in
+        let* (coqtop, args) =
+          let open Memo.Build.O in
+          Build_system.run_exn (fun () ->
+              let* dc = Dune_rules.Dir_contents.get sctx ~dir in
+              let* coq_src = Dune_rules.Dir_contents.coq dc in
+              let coq_module =
+                let source = coq_file_build in
+                match Dune_rules.Coq_sources.find_module ~source coq_src with
+                | Some m -> snd m
+                | None ->
+                    let hints =
+                      [ Pp.textf "is the file part of a stanza?"
+                      ; Pp.textf "has the file been written to disk?" ]
+                    in
+                    User_error.raise ~hints
+                      [ Pp.textf "cannot find file: %s" coq_file_arg ]
+              in
+              let stanza =
+                Dune_rules.Coq_sources.lookup_module coq_src coq_module
+              in
+              let* (args, boot_type) =
+                match stanza with
+                | None ->
+                    User_error.raise
+                      [ Pp.textf "file not part of any stanza: %s" coq_file_arg ]
+                | Some (`Theory theory) ->
+                    Dune_rules.Coq_rules.coqtop_args_theory ~sctx ~dir
+                      ~dir_contents:dc theory coq_module
+                | Some (`Extraction extr) ->
+                    Dune_rules.Coq_rules.coqtop_args_extraction ~sctx ~dir
+                      ~dir_contents:dc extr
+              in
+              let* _ : unit * Dep.Fact.t Dep.Map.t =
+                let deps =
+                  Dune_rules.Coq_rules.deps_of ~dir ~boot_type coq_module
+                in
+                Action_builder.run deps Eager
+              in
+              let* (args, _) : string list * Dep.Fact.t Dep.Map.t =
+                let args =
+                  let dir = Path.external_ (Path.External.initial_cwd) in
+                  Dune_rules.Command.expand ~dir (S args)
+                in
+                Action_builder.run args.build Eager
+              in
+              let* prog =
+                Super_context.resolve_program sctx ~dir ~loc:None coqtop
+              in
+              let prog = Action.Prog.ok_exn prog in
+              let+ _ : Digest.t = Build_system.build_file prog in
+              (Path.to_string prog, args))
+        in
+        let argv =
+          let topfile =
+            Path.to_absolute_filename (Path.build coq_file_build)
+          in
+          coqtop :: "-topfile" :: topfile :: args @ extra_args
+        in
+        let env = Super_context.context_env sctx in
+        Fiber.return (coqtop, argv, env))
+  in
+  restore_cwd_and_execve common coqtop argv env
+
+let command = (term, info)

bin/coqtop.mli

@@ -0,0 +1 @@
+val command : unit Cmdliner.Term.t * Cmdliner.Term.info

bin/main.ml

@@ -30,7 +30,7 @@ let all : _ Term.Group.t list =
     ]
     |> List.map ~f:in_group
   in
-  let groups = [ Ocaml.group; Rpc.group; Internal.group ] in
+  let groups = [ Ocaml.group; Coq.group; Rpc.group; Internal.group ] in
   terms @ groups
 
 (* Short reminders for the most used and useful commands *)

doc/usage.rst

@@ -613,3 +613,34 @@ match with available configurations.
 For example, if you use the ``cppo`` preprocessor to generate the file
 ``real_module_name.ml``, then the source file could be named
 ``real_module_name.cppo.ml``.
+
+Running a Coq Toplevel
+======================
+
+Dune supports running a Coq toplevel like ``coqtop``, which is typically used
+for Coq to interact with proof editors like CoqIDE or Proof General.
+
+.. code:: bash
+
+   $ dune coq top <file> -- <args>
+
+Run a Coq toplevel (``coqtop`` by default) on the given Coq file ``<file>``,
+after having re-compiled its dependencies if necessary. The given arguments
+``<args>`` are forwarded to the invoked command. For example, this can be used
+to pass a ``-emacs`` flag to ``coqtop``.
+
+A different toplevel can be chosen with ``dune coq top --toplevel CMD <file>``.
+Note that using ``--toplevel echo`` is one way to observe what options are
+actually passed to the toplevel. These options are computed based on the
+options that would be passed to the Coq compiler if it was invoked on the Coq
+file ``<file>``.
+
+Limitations
+-----------
+
+* Only files that are part of a stanza can be loaded in a Coq toplevel.
+* When a file is created, it must be written to the file system before the Coq
+  toplevel is started.
+* When new dependencies are added to a file (via a Coq ``Require`` vernacular
+  command), it is in principle required to save the file and restart to Coq
+  toplevel process.

otherlibs/stdune/fpath.ml

@@ -69,6 +69,29 @@ let follow_symlink path =
   | Ok (Some p) -> loop 20 p
   | Error e -> Error (Unix_error e)
 
+let rec follow_symlinks path =
+  let parent = Filename.dirname path in
+  let file = Filename.basename path in
+  (* If we reached the root, just return the path. *)
+  if parent = path then Some path else
+  if parent = Filename.current_dir_name then
+    (* Only keep the initial ["."] if it was in the path. *)
+    if path = Filename.concat Filename.current_dir_name file then
+      Some path
+    else
+      Some file
+  else
+    (* Recurse on parent, and re-add toplevel file. *)
+    match follow_symlinks parent with
+    | None -> None
+    | Some parent ->
+        let path = Filename.concat parent file in
+        (* Nomalize the result. *)
+        match follow_symlink path with
+        | Ok p -> Some p
+        | Error Max_depth_exceeded -> None
+        | Error _ -> Some path
+
 let win32_unlink fn =
   try Unix.unlink fn
   with Unix.Unix_error (Unix.EACCES, _, _) as e -> (

otherlibs/stdune/fpath.mli

@@ -21,6 +21,12 @@ type follow_symlink_error =
 
 val follow_symlink : string -> (string, follow_symlink_error) result
 
+(** [follow_symlinks path] returns a file path that is equivalent to [path],
+    but free of symbolic links. The value [None] is returned if the maximum
+    symbolic link dept is reached (i.e., [follow_symlink] returns the value
+    [Error Max_depth_exceeded] on some intermediate path). *)
+val follow_symlinks : string -> string option
+
 val unlink : string -> unit
 
 val unlink_no_err : string -> unit

otherlibs/stdune/map.ml

@@ -239,6 +239,14 @@ module Make (Key : Key) : S with type key = Key.t = struct
               (match v with
               | None -> entries
               | Some x -> List.append x entries))
+
+    let find_elt : type a. a t -> f:(a -> bool) -> (key * a) option =
+      fun m ~f ->
+      let exception Found of (key * a) in
+      try
+        let check_found k e = if f e then raise_notrace (Found (k, e)) in
+        iteri ~f:(fun k -> List.iter ~f:(check_found k)) m; None
+      with Found p -> Some p
   end
 
   exception Found of Key.t

otherlibs/stdune/map_intf.ml

@@ -151,5 +151,11 @@ module type S = sig
     val find : 'a t -> key -> 'a list
 
     val add_all : 'a t -> key -> 'a list -> 'a t
+
+    (** [find_elt m ~f] linearly traverses the map [m] and the contained lists
+        to find the first element [e] (in a list [l], mapped to key [k]) such
+        that [f e = true]. If such an [e] is found then the function returns
+        [Some (k,e)], otherwise it returns [None]. *)
+    val find_elt : 'a t -> f:('a -> bool) -> (key * 'a) option
   end
 end

src/dune_rules/command.mli

@@ -104,3 +104,11 @@ module Ml_kind : sig
 
   val ppx_driver_flag : Ml_kind.t -> _ Args.t
 end
+
+(** [expand ~dir args] interprets the command line arguments [args] to produce
+    corresponding strings, assuming they will be used as arguments to run a
+    command in directory [dir]. *)
+val expand :
+  dir:Path.t ->
+  'a Args.t ->
+  string list Action_builder.With_targets.t

src/dune_rules/coq_module.ml

@@ -21,13 +21,32 @@ module Name = struct
   let to_string s = s
 end
 
-(* We keep prefix and name separated as the handling of `From Foo Require Bar.`
-   may benefit from it. *)
-type t =
-  { source : Path.Build.t
-  ; prefix : string list
-  ; name : Name.t
-  }
+module Module = struct
+  (* We keep prefix and name separated as the handling of `From Foo Require Bar.`
+     may benefit from it. *)
+  type t =
+    { source : Path.Build.t
+    ; prefix : string list
+    ; name : Name.t
+    }
+
+  let compare { source; prefix; name } t =
+    let open Ordering.O in
+    let= () = Path.Build.compare source t.source in
+    let= () = List.compare prefix t.prefix ~compare:String.compare in
+    Name.compare name t.name
+
+  let to_dyn { source; prefix; name } =
+    Dyn.record
+      [ ("source", Path.Build.to_dyn source)
+      ; ("prefix", Dyn.list Dyn.string prefix)
+      ; ("name", Name.to_dyn name)
+      ]
+end
+
+include Module
+
+module Map = Map.Make(Module)
 
 let make ~source ~prefix ~name = { source; prefix; name }
 

src/dune_rules/coq_module.mli

@@ -22,6 +22,8 @@ end
 
 type t
 
+module Map : Map.S with type key = t
+
 (** A Coq module [a.b.foo] defined in file [a/b/foo.v] *)
 val make :
      source:Path.Build.t

src/dune_rules/coq_rules.ml

@@ -447,6 +447,26 @@ let setup_rules ~sctx ~dir ~dir_contents (s : Theory.t) =
       let { Module_rule.coqc; coqdep } = setup_rule cctx ~source_rule m in
       [ coqc; coqdep ])
 
+let coqtop_args_theory ~sctx ~dir ~dir_contents (s : Theory.t) coq_module =
+  let name = snd s.name in
+  let scope = SC.find_scope_by_dir sctx dir in
+  let coq_lib_db = Scope.coq_libs scope in
+  let theory = Coq_lib.DB.resolve coq_lib_db s.name |> Result.ok_exn in
+  let* coq_dir_contents = Dir_contents.coq dir_contents in
+  let+ cctx =
+    let wrapper_name = Coq_lib.wrapper theory in
+    let theories_deps =
+      Coq_lib.DB.requires coq_lib_db theory |> Resolve.of_result
+    in
+    let theory_dirs = Coq_sources.directories coq_dir_contents ~name in
+    let theory_dirs = Path.Build.Set.of_list theory_dirs in
+    let coqc_dir = (Super_context.context sctx).build_dir in
+    Context.create sctx ~coqc_dir ~dir ~wrapper_name ~theories_deps ~theory_dirs
+      s.buildable
+  in
+  let cctx = Context.for_module cctx coq_module in
+  (Context.coqc_file_flags cctx, cctx.boot_type)
+
 (******************************************************************************)
 (* Install rules *)
 (******************************************************************************)
@@ -571,3 +591,23 @@ let extraction_rules ~sctx ~dir ~dir_contents (s : Extraction.t) =
   let { Module_rule.coqc; coqdep } = setup_rule cctx ~source_rule coq_module in
   let coqc = Action_builder.With_targets.add coqc ~file_targets:ml_targets in
   [ coqdep; coqc ]
+
+let coqtop_args_extraction ~sctx ~dir ~dir_contents (s : Extraction.t) =
+  let* cctx =
+    let wrapper_name = "DuneExtraction" in
+    let theories_deps =
+      let scope = SC.find_scope_by_dir sctx dir in
+      let coq_lib_db = Scope.coq_libs scope in
+      Resolve.of_result
+        (Coq_lib.DB.requires_for_user_written coq_lib_db s.buildable.theories)
+    in
+    let theory_dirs = Path.Build.Set.empty in
+    Context.create sctx ~coqc_dir:dir ~dir ~wrapper_name ~theories_deps
+      ~theory_dirs s.buildable
+  in
+  let+ coq_module =
+    let+ coq = Dir_contents.coq dir_contents in
+    Coq_sources.extract coq s
+  in
+  let cctx = Context.for_module cctx coq_module in
+  (Context.coqc_file_flags cctx, cctx.boot_type)