Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

Removing custom support for compiler hacking #114

Open
wants to merge 1 commit into
base: master
Choose a base branch
from
Open

Removing custom support for compiler hacking #114

Changes from all commits
Commits
Show all changes
1 commit
Select commit
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
31 changes: 1 addition & 30 deletions fstar-mode.el
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -5090,10 +5090,6 @@ includes a Tramp prefix)."
(buffer-disable-undo)
(current-buffer))))

(defun fstar-subp-prover-args-safe-p (args)
"Check whether ARGS is a known-safe value for `fstar-subp-prover-args'."
(equal args 'fstar-subp-prover-args-for-compiler-hacking))

(defcustom fstar-subp-prover-args nil
"Arguments to pass to F* in interactive mode.

Expand Down Expand Up @@ -5125,8 +5121,7 @@ evaluating (fstar-subp-get-prover-args). Note that passing
multiple arguments as one string will not work: you should use
\\='(\"--aa\" \"--bb\"), not \"--aa --bb\"."
:group 'fstar
:type '(repeat string)
:safe #'fstar-subp-prover-args-safe-p)
:type '(repeat string))

(defcustom fstar-subp-prover-additional-args nil
"Additional arguments to pass to F* in interactive mode.
Expand Down Expand Up @@ -5178,30 +5173,6 @@ Non-nil NO-IDE means don't include `--ide' and `--in'."
(fstar-subp--parse-prover-args fstar-subp-prover-additional-args))))
`(,(fstar-subp--buffer-file-name) ,@ide-flag "--smt" ,smt-path ,@usr-args)))

(defun fstar-subp--prover-includes-for-compiler-hacking ()
"Compute a list of folders to include for hacking on the F* compiler."
(-if-let* ((fname (buffer-file-name))
(default-directory (locate-dominating-file fname "_tags")))
(let ((exclude-list '("." ".." "VS" "tests" "tools" "boot_fstis"
"ocaml-output" "u_ocaml-output" "u_boot_fsts"))
(src-dir (expand-file-name "src" default-directory))
(include-dirs nil))
(push (expand-file-name "ulib") include-dirs)
(dolist (dir (directory-files src-dir nil))
(unless (member dir exclude-list)
(let ((fulldir (expand-file-name dir src-dir)))
(when (file-directory-p fulldir)
(push fulldir include-dirs)))))
(nreverse include-dirs))
(user-error (concat "Couldn't find _tags file while trying to "
" set up F*-mode for compiler hacking."))))

(defun fstar-subp-prover-args-for-compiler-hacking ()
"Compute arguments suitable for hacking on the F* compiler."
`("--eager_inference" "--lax" "--MLish" "--warn_error" "-272"
,@(-mapcat (lambda (dir) `("--include" ,dir))
(fstar-subp--prover-includes-for-compiler-hacking))))

(defvar fstar-subp--default-directory nil
"Directory in which to start F*.

Expand Down