Open aseemr opened 5 years ago
Hi Aseem,
I recently added support for typechecking the F typechecker source files in the emacs mode via Makefile(s) and the -in targets. This helps keep the F command line options etc. consistent between bootstrapping via the command line and in the emacs mode.
I didn't quite get that part :) Can you say more about how this works? Does it start Emacs with the right options?
If fstar-subp-prover-args-safe-p goes away
There's to ways to proceed: either make the function always return nil, or remove the :safe
predicate entirely. I would go with the second one.
Hi Clement:
It's through the %.fs-in
targets in makefiles. For example, see the last line here: https://github.com/FStarLang/FStar/blob/master/src/Makefile.boot.common. Most of us have a small script in .emacs
that finds such a target in the Makefile, invokes it to get the F* options, and then sets the fstar-subp-prover-args
with those. This Makefile.boot.common is then included by makefiles in various src/
directories (e.g. https://github.com/FStarLang/FStar/blob/master/src/smtencoding/Makefile). We have been using it for hacl, mitls, etc.
I filed a PR. Thanks!
Most of us have a small script in .emacs that finds such a target in the Makefile, invokes it to get the F* options, and then sets the fstar-subp-prover-args with those.
Did you consider moving that to fstar-mode, so that everyone has it by default? I think that could be a better option than just removing the custom support entirely.
That's a good idea, I hadn't thought about that. But in that case, the support will be for all F files, and not just the typechecker ones, so the code that is removed in the PR should still go away? Also note that the options from fstar-subp-prover-args-for-compiler-hacking
are already obsolete, e.g. --eager_inference
is no longer a valid F option.
The following is the snippet from .emacs
that looks for the F* options in the makefile:
(defun my-fstar-compute-prover-args-using-make ()
"Construct arguments to pass to F* by calling make."
(with-demoted-errors "Error when constructing arg string: %S"
(let* ((fname (file-name-nondirectory buffer-file-name))
(target (concat fname "-in"))
(argstr (condition-case nil
(car (process-lines "make" "--quiet" target))
(error (concat //some default options that can be null//
)))))
(split-string argstr))))
(setq fstar-subp-prover-args #'my-fstar-compute-prover-args-using-make)
But in that case, the support will be for all F* files, and not just the typechecker ones, so the code that is removed in the PR should still go away?
Not quite: we would add this fstar-compute-prover-args-using-make
function to fstar-mode, then mark that as a safe value. Then all that projects would have to do is to add a .dir-locals.el that sets fstar-subp-prover-args to that function.
You are probably right, I don't know what is a safe value. The way I was thinking it would work is: we would add this fstar-compute-prover-args-using-make
function to fstar-mode.el
. Before starting F, F mode executes this function and sets the fstar-subp-prover-args
with the output. I am not sure why do we need .dir-locals.el
. And note that this fstar-compute-prover-args-using-make
would work for both the compiler files and other F* files alike, so fstar-subp--prover-includes-for-compiler-hacking
, fstar-subp-prover-args-for-compiler-hacking
, etc. won't be needed (they are already dead code currently).
Hi Clement:
I recently added support for typechecking the F typechecker source files in the emacs mode via Makefile(s) and the
-in
targets. This helps keep the F command line options etc. consistent between bootstrapping via the command line and in the emacs mode.I also noticed that there is a
fstar-subp-prover-args-for-compiler-hacking
infstar-mode.el
, perhaps we should get rid of that? I tried to clean it up, basically removing it and anything that uses it, but got stuck at https://github.com/FStarLang/fstar-mode.el/blob/master/fstar-mode.el#L5129. Iffstar-subp-prover-args-safe-p
goes away, not sure what should happen at this line.What do you think?
Thanks,
-Aseem.