The Coq mailing list

[S�bastien Hinderer <Sebastien.Hinderer AT ens-lyon.fr>]

Dear Coq users and developers,

It seemed to me it could be useful to be able to specify from the command
line that one wants to load a file in coqtop, but verbosely. This seemed
indeed simpler than running coqtop and then enterening the command :

Loae Verbose f.

In particular, this would permit to benefit from shell history facilities
when one wants to load one file during several consecutive sessions under
coqtop.

However, I didn't find any way to do that properly in Coq v8.0-beta.
So, I slightly modified Coq sources, and added two new options :
-load-vernac-source-verbose f and its shorter equivalent -lv f.

For me, it works just fine, so I attach the corresponding patch to this
mail.

To apply this patch, do :

cd $COQTOP
patch -p1 < thepatch

And then just recompile Coq with 

make world

Coq developpers : if you find the patch useful, I'd be glad to see it
integrated into a future Coq distribution.

Best wishes,
Sébastien.
diff -ur coq-8.0beta/toplevel/coqtop.ml 
coq-8.0beta-modified/toplevel/coqtop.ml
--- coq-8.0beta/toplevel/coqtop.ml      2003-12-30 10:56:20.000000000 +0100
+++ coq-8.0beta-modified/toplevel/coqtop.ml     2004-01-15 06:40:08.000000000 
+0100
@@ -73,16 +73,16 @@
 let set_default_include d = set_include d Nameops.default_root_prefix
 let set_default_rec_include d = set_rec_include d Nameops.default_root_prefix
  
-let load_vernacular_list = ref ([] : string list)
-let add_load_vernacular s =
-  load_vernacular_list := (make_suffix s ".v") :: !load_vernacular_list
+let load_vernacular_list = ref ([] : (string * bool) list)
+let add_load_vernacular verb s =
+  load_vernacular_list := ((make_suffix s ".v"),verb) :: 
!load_vernacular_list
 let load_vernacular () =
   List.iter
-    (fun s -> 
+    (fun (s,b) -> 
       if Options.do_translate () then
-       with_option translate_file (Vernac.load_vernac false) s
+       with_option translate_file (Vernac.load_vernac b) s
       else
-       Vernac.load_vernac false s)
+       Vernac.load_vernac b s)
     (List.rev !load_vernacular_list)
 
 let load_vernacular_obj = ref ([] : string list)
@@ -192,9 +192,13 @@
     | "-load-ml-source" :: []       -> usage ()
 
     | ("-load-vernac-source"|"-l") :: f :: rem -> 
-       add_load_vernacular f; parse rem
+       add_load_vernacular false f; parse rem
     | ("-load-vernac-source"|"-l") :: []       -> usage ()
 
+    | ("-load-vernac-source-verbose"|"-lv") :: f :: rem -> 
+       add_load_vernacular true f; parse rem
+    | ("-load-vernac-source-verbose"|"-lv") :: []       -> usage ()
+
     | "-load-vernac-object" :: f :: rem -> add_vernac_obj f; parse rem
     | "-load-vernac-object" :: []       -> usage ()
 
diff -ur coq-8.0beta/toplevel/usage.ml coq-8.0beta-modified/toplevel/usage.ml
--- coq-8.0beta/toplevel/usage.ml       2002-11-05 17:59:14.000000000 +0100
+++ coq-8.0beta-modified/toplevel/usage.ml      2004-01-15 06:39:26.000000000 
+0100
@@ -34,6 +34,8 @@
   -load-ml-source f      load ML file f 
   -load-vernac-source f  load Coq file f.v (Load f.)
   -l f                   (idem) 
+  -load-vernac-source-verbose f  load Coq file f.v (Load Verbose f.)
+  -lv f                        (idem)
   -load-vernac-object f  load Coq object file f.vo
   -require f             load Coq object file f.vo and import it (Require f.)
   -compile f             compile Coq file f.v (implies -batch)