forked from naveensundarg/DCECProver
-
Notifications
You must be signed in to change notification settings - Fork 0
/
Copy pathloader.lisp
48 lines (41 loc) · 1.83 KB
/
loader.lisp
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
(defparameter *ql-modules*
(list "fiveam" "optima" "gtfl"))
(mapcar #'quicklisp:quickload *ql-modules*)
(load (format NIL "~asnark-20120808r022/snark-system.lisp" *default-pathname-defaults*))
(make-snark-system)
(let*((reg-pathname (make-pathname :directory (pathname-directory *load-truename*)))
(path-present NIL))
(dolist (pathname asdf:*central-registry*)
(when (equalp pathname reg-pathname)
(setf path-present T)))
(unless path-present
(push (make-pathname :directory (pathname-directory *load-truename*)) asdf:*central-registry*)))
(quicklisp:quickload "getopt")
(asdf:defsystem :shadowprover
:serial t
:description "A prover for DCEC, a first-order modal logic."
:author "Naveen Sundar G."
:license "MIT BSD"
:depends-on (#:optima #:fiveam #:gtfl)
:components ((:file "package")
(:file "configs")
(:file "params")
(:file "./snark-20120808r022/snark-interface")
(:file "./utils/misc")
(:file "./utils/syntax")
(:file "./utils/sorts")
(:file "./inference-rules/expanders")
(:file "./inference-rules/backward-rules")
(:file "./inference-rules/folrules")
(:file "./inference-rules/primitiverules")
(:file "./inference-rules/derivedrules")
(:file "./utils/show")
(:file "ShadowProver")
(:file "converter")
(:file "./tests/dev-tests")
(:file "./projects/akrasia/akrasia")
(:file "./projects/false-belief-task/false-belief-task")
(:file "./projects/wise-men-puzzle/wise-men-puzzle")
(:file "./projects/knights-and-knaves/knights-and-knaves")
(:file "./tests/all-tests")))
(asdf:load-system :shadowprover)