Cleanup of compiler hacking subp-prover args in fstar-mode.el

[aseemr]

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 in fstar-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. If fstar-subp-prover-args-safe-p goes away, not sure what should happen at this line.

What do you think?

Thanks,

-Aseem.

[cpitclaudel]

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.

[aseemr]

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!

[cpitclaudel]

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.

[aseemr]

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)

[cpitclaudel]

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.

[aseemr]

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).