Comments (6)
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.
from fstar-mode.el.
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!
from fstar-mode.el.
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.
from fstar-mode.el.
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)
from fstar-mode.el.
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.
from fstar-mode.el.
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).
from fstar-mode.el.
Related Issues (20)
- F* over TRAMP crashes HOT 17
- No company completion HOT 4
- fstar-mode over docker-tramp HOT 5
- fstar-jump-to-definition on a module should jump to the fsti if it exists HOT 1
- Code that typechecks normally from the command line can crash fstar-mode HOT 1
- `nil` confusion HOT 2
- fslit seems to no longer work very well HOT 6
- can't include file in subdirectory with fslit HOT 4
- Weird display of the highlighted blocks HOT 1
- Highlight sladmit
- c-c c-v verify should ask to save the current file HOT 5
- fstar literate setup problems on Ubuntu 22.04 and emacs 28 HOT 4
- Not all errors going to *Flycheck errors*
- Open not always working HOT 1
- c-c c-r reload better description HOT 3
- elaborate trace mode HOT 2
- Definition lookup works only once
- Using F* remotely, over TRAMP HOT 5
- advancing is missing a bunch of new top-level constructs HOT 2
Recommend Projects
-
React
A declarative, efficient, and flexible JavaScript library for building user interfaces.
-
Vue.js
🖖 Vue.js is a progressive, incrementally-adoptable JavaScript framework for building UI on the web.
-
Typescript
TypeScript is a superset of JavaScript that compiles to clean JavaScript output.
-
TensorFlow
An Open Source Machine Learning Framework for Everyone
-
Django
The Web framework for perfectionists with deadlines.
-
Laravel
A PHP framework for web artisans
-
D3
Bring data to life with SVG, Canvas and HTML. 📊📈🎉
-
Recommend Topics
-
javascript
JavaScript (JS) is a lightweight interpreted programming language with first-class functions.
-
web
Some thing interesting about web. New door for the world.
-
server
A server is a program made to process requests and deliver data to clients.
-
Machine learning
Machine learning is a way of modeling and interpreting data that allows a piece of software to respond intelligently.
-
Visualization
Some thing interesting about visualization, use data art
-
Game
Some thing interesting about game, make everyone happy.
Recommend Org
-
Facebook
We are working to build community through open source technology. NB: members must have two-factor auth.
-
Microsoft
Open source projects and samples from Microsoft.
-
Google
Google ❤️ Open Source for everyone.
-
Alibaba
Alibaba Open Source for everyone
-
D3
Data-Driven Documents codes.
-
Tencent
China tencent open source team.
from fstar-mode.el.