wip

coq/files.ml

@@ -35,17 +35,31 @@ module Require_result = struct
     | Wait of CUnix.physical_path list
 end
 
+let pp_bind fmt (file, dp) = Stdlib.Format.fprintf fmt "@[%s / %s@]" file (Names.DirPath.to_string dp)
+
+let pp_partials fmt lp = Stdlib.Format.(fprintf fmt "@[%a@]" (pp_print_list pp_bind) lp)
+
 let check_file_ready ?root (m, _imports) =
-  match Loadpath.locate_qualified_library ?root m with
-  | Ok (dirpath, file) ->
+  let dir, _base = Libnames.repr_qualid m in
+  match Loadpath.expand_path ?root dir with
+  | [], [] -> Error "file not found in loadpath, both empty"
+  | [], partials ->
+    Stdlib.Format.eprintf "partial match:@\n @[%a@]%!" pp_partials partials;
+    Error "weird stuff happened in expand path"
+  | (file, dp) :: rr, _ -> (
     let () =
-      Stdlib.Format.eprintf "found file: %s for library %s@\n%!" file
-        (Names.DirPath.to_string dirpath)
+      Stdlib.Format.eprintf "exact match: %a@\n%!" pp_partials ((file, dp) :: rr)
     in
-    let ready = true in
-    (* Hook for the document manager *)
-    if ready then Ok (Ok (dirpath, file)) else Error file
-  | Error e -> Ok (Error e)
+    match Loadpath.locate_qualified_library ?root m with
+    | Ok (dirpath, file) ->
+      let () =
+        Stdlib.Format.eprintf "found object file: %s for library %s@\n%!" file
+          (Names.DirPath.to_string dirpath)
+      in
+      let ready = true in
+      (* Hook for the document manager *)
+      if ready then Ok (Ok (dirpath, file)) else Error file
+    | Error e -> Ok (Error e))
 
 let requires_are_ready ~files:_ { Ast.Require.from; export = _; mods; _ } =
   let root = Option.map ~f:qualid_to_dirpath from in

coq/files.mli

@@ -31,3 +31,4 @@ module Require_result : sig
 end
 
 val requires_are_ready : files:t -> Ast.Require.t -> Require_result.t
+val intern : Names.DirPath.t -> Library.library_t

examples/ex0.v

@@ -11,6 +11,16 @@ Proof. by elim: n. Qed.
 
 Definition m := addn0.
 
+Theorem foo n : n = n :> nat.
+Proof.
+aa.
+bb. slkjd. skl . skj .
+cc.
+dd.
+Qed.
+
+About foo.
+
 Print m.
 
 Definition a := 2.

test/compiler/basic/proj1/a.v

@@ -1,7 +1,11 @@
+From Coq Require Reals.
+
 Definition aa := 3.
 
 Lemma foo : True.
-Proof.
+Proof. 
 (* Some comment *)
-auto.
+auto .
 Qed.
+
+Optimize Heap.

test/compiler/basic/proj1/b.v

@@ -1,2 +1,6 @@
+From Coq Require Reals.
+
 Require a.
-Definition bb := a.aa.
+Definition bb := a.aa. 
+
+Optimize Heap.