1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
|
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
open Vernac
open Vernacexpr
open Pfedit
open Pp
open Util
open Names
open Term
open Printer
open Environ
open Evarutil
open Evd
open Hipattern
open Tacmach
open Reductionops
open Termops
open Namegen
open Ideutils
open Compat
type coqtop = {
mutable cout : in_channel ;
mutable cin : out_channel ;
}
let dummy_coqtop = {
cout = stdin ;
cin = stdout ;
}
let prerr_endline s = if !debug then prerr_endline s else ()
let output = ref (Format.formatter_of_out_channel stdout)
let msg m =
let b = Buffer.create 103 in
Pp.msg_with (Format.formatter_of_buffer b) m;
Buffer.contents b
let msgnl m =
(msg m)^"\n"
let init () = List.tl (Array.to_list Sys.argv)
(* Coqtop.init_ide (List.tl (Array.to_list Sys.argv))*)
let i = ref 0
let get_version_date () =
let date =
if Glib.Utf8.validate Coq_config.date
then Coq_config.date
else "<date not printable>" in
try
let ch = open_in (Coq_config.coqsrc^"/revision") in
let ver = input_line ch in
let rev = input_line ch in
(ver,rev)
with _ -> (Coq_config.version,date)
let short_version () =
let (ver,date) = get_version_date () in
Printf.sprintf "The Coq Proof Assistant, version %s (%s)\n" ver date
let version () =
let (ver,date) = get_version_date () in
Printf.sprintf
"The Coq Proof Assistant, version %s (%s)\
\nArchitecture %s running %s operating system\
\nGtk version is %s\
\nThis is the %s version (%s is the best one for this architecture and OS)\
\n"
ver date
Coq_config.arch Sys.os_type
(let x,y,z = GMain.Main.version in Printf.sprintf "%d.%d.%d" x y z)
(if Mltop.is_native then "native" else "bytecode")
(if Coq_config.best="opt" then "native" else "bytecode")
exception Coq_failure of (Util.loc * Pp.std_ppcmds)
let eval_call coqtop (c:'a Ide_blob.call) =
Safe_marshal.send coqtop.cin c;
let res = (Safe_marshal.receive: in_channel -> 'a Ide_blob.value) coqtop.cout in
match res with
| Ide_blob.Good v -> v
| Ide_blob.Fail (l,pp) -> prerr_endline (msg pp); raise (Coq_failure (l,pp))
let is_in_loadpath coqtop s = eval_call coqtop (Ide_blob.is_in_loadpath s)
let reset_initial = Ide_blob.reinit
let raw_interp coqtop s = eval_call coqtop (Ide_blob.raw_interp s)
let interp coqtop b s = eval_call coqtop (Ide_blob.interp b s)
let rewind coqtop i = eval_call coqtop (Ide_blob.rewind i)
let read_stdout coqtop = eval_call coqtop Ide_blob.read_stdout
let spawn_coqtop () =
let prog = Sys.argv.(0) in
let dir = Filename.dirname prog in
let oc,ic = Unix.open_process (dir^"/coqtop.opt -ideslave") in
{ cin = ic; cout = oc }
let kill_coqtop coqtop = raw_interp coqtop "Quit."
let reset_coqtop coqtop =
kill_coqtop coqtop;
let ni = spawn_coqtop () in
coqtop.cin <- ni.cin;
coqtop.cout <- ni.cout
module PrintOpt =
struct
type t = string list
let implicit = ["Implicit"]
let coercions = ["Coercions"]
let raw_matching = ["Matching";"Synth"]
let notations = ["Notations"]
let all_basic = ["All"]
let existential = ["Existential Instances"]
let universes = ["Universes"]
let state_hack = Hashtbl.create 11
let _ = List.iter (fun opt -> Hashtbl.add state_hack opt false)
[ implicit; coercions; raw_matching; notations; all_basic; existential; universes ]
let set coqtop opt value =
Hashtbl.replace state_hack opt value;
List.iter
(fun cmd ->
let str = (if value then "Set" else "Unset") ^ " Printing " ^ cmd ^ "." in
raw_interp coqtop str)
opt
let enforce_hack coqtop = Hashtbl.iter (set coqtop) state_hack
end
let rec is_pervasive_exn = function
| Out_of_memory | Stack_overflow | Sys.Break -> true
| Error_in_file (_,_,e) -> is_pervasive_exn e
| Loc.Exc_located (_,e) -> is_pervasive_exn e
| DuringCommandInterp (_,e) -> is_pervasive_exn e
| _ -> false
let print_toplevel_error exc =
let (dloc,exc) =
match exc with
| DuringCommandInterp (loc,ie) ->
if loc = dummy_loc then (None,ie) else (Some loc, ie)
| _ -> (None, exc)
in
let (loc,exc) =
match exc with
| Loc.Exc_located (loc, ie) -> (Some loc),ie
| Error_in_file (s, (_,fname, loc), ie) -> None, ie
| _ -> dloc,exc
in
match exc with
| End_of_input -> str "Please report: End of input",None
| Vernacexpr.Drop -> str "Drop is not allowed by coqide!",None
| Vernacexpr.Quit -> str "Quit is not allowed by coqide! Use menus.",None
| _ ->
(try Cerrors.explain_exn exc with e ->
str "Failed to explain error. This is an internal Coq error. Please report.\n"
++ str (Printexc.to_string e)),
(if is_pervasive_exn exc then None else loc)
let process_exn e = let s,loc= print_toplevel_error e in (msgnl s,loc)
type tried_tactic =
| Interrupted
| Success of int (* nb of goals after *)
| Failed
let goals coqtop =
PrintOpt.enforce_hack coqtop;
eval_call coqtop Ide_blob.current_goals
let make_cases coqtop s = eval_call coqtop (Ide_blob.make_cases s)
let current_status coqtop = eval_call coqtop Ide_blob.current_status
|
