blob: e2d06e00fe5f3e49ef796d5de15abbf686530f76 (
plain)
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
|
(defvar ml4pg-home-dir (concatenate 'string proof-home-directory "contrib/ML4PG/"))
(defconst *matlab-program* nil)
(defconst *weka-dir* (concatenate 'string proof-home-directory "contrib/ML4PG/weka.jar"))
(defvar ml4pg-mode nil)
(defun ml4pg-select-mode ()
(interactive)
(let ((smode (read-string "What mode do you want to use (Coq -> c (default), SSReflect -> s): ")))
(setq ml4pg-mode smode)
(cond ((string= ml4pg-mode "s")
(progn (load-file (concat ml4pg-home-dir "ssreflect/auxiliary_files.el"))
(load-file (concat ml4pg-home-dir "ssreflect/feature_extraction_2.el"))
(load-file (concat ml4pg-home-dir "ssreflect/matlab_interaction.el"))
(load-file (concat ml4pg-home-dir "ssreflect/shortcuts.el"))
(load-file (concat ml4pg-home-dir "ssreflect/menus.el"))
(load-file (concat ml4pg-home-dir "ssreflect/storage.el"))
(load-file (concat ml4pg-home-dir "ssreflect/save_lemmas.el"))
(load-file (concat ml4pg-home-dir "ssreflect/weka.el"))
(ml4pg-init-clusters)
(ml4pg-activate-icons)
(ml4pg-exported-libraries)
))
(t (progn (load-file (concat ml4pg-home-dir "coq/auxiliary_files.el"))
(load-file (concat ml4pg-home-dir "coq/feature_extraction.el"))
(load-file (concat ml4pg-home-dir "coq/matlab_interaction.el"))
(load-file (concat ml4pg-home-dir "coq/shortcuts.el"))
(load-file (concat ml4pg-home-dir "coq/menus.el"))
(load-file (concat ml4pg-home-dir "coq/storage.el"))
(load-file (concat ml4pg-home-dir "coq/save_lemmas.el"))
(load-file (concat ml4pg-home-dir "coq/weka.el"))
(ml4pg-init-clusters)
(ml4pg-activate-icons)
(ml4pg-exported-libraries)
))
))
(let ((ex? (read-string "Do you want to extract the features of the lemmas of this library (Yes -> y, No -> n): ")))
(if (string= ex? "y")
(progn (let ((b (buffer-name)))
(ml4pg-extract-theorems-library)
(delete-other-windows)
(switch-to-buffer-other-window "*display*")
(delete-other-windows)
(switch-to-buffer-other-window b)
(delete-other-windows)
(proof-shell-invisible-cmd-get-result (format "Unset Printing All"))
))
nil
)))
|
