Hi Julien, Thank you for your questions. Since the set of people who can answer all these questions at once is rather small, I'll try to answer some, hoping that others will add to this.
On Sun, Sep 17, 2017 at 7:53 PM, Julien Cretin via fstar-club < fstar-club@lists.gforge.inria.fr> wrote: > Hi list, > > I have a few random questions if any of you have time to answer any of > them. > > 1. What is the difference between list and seq? Is it only the fact that > seq is abstract? Is it to have faster proofs and clearer API? > `seq` is indeed an abstract version of `list`. The goal is to hide the list representation and provide instead lemmas with quantifier patterns that should make for better SMT automation. This is amazing when it works ... but it can also be a pain sometimes: https://github.com/FStarLang/FStar/issues/1208 2. How can I get rid of subscripts in fstar-mode in emacs? When I type > "foo42", I get $foo_{42}$. I already managed to get rid of > prettify-symbols-mode and visual-line-mode, but this one seems to be part > of fstar-mode. > This is indeed a feature I would also like to be able to turn off. Clement? 3. Is it possible (and does it make sense) to define an effect for > normalizing computations with a state? From what I understand (and test) > STATE computations may diverge. I tried to alias PURE as FOO and I was able > to write a loop: > > module Foo > > >> new_effect FOO = PURE >> sub_effect PURE ~> FOO = fun _ wp -> wp > > >> let rec loop _: FOO unit (fun p -> p ()) = loop () > > > So I suspect that it is not possible to have such effect (termination + > state). > It is possible to define a terminating variant of state. You need to use the still experimental "DM4F feature" ( https://www.fstar-lang.org/papers/dm4free/) to define the effect, but it works and you can find a simple example in https://github.com/FStarLang/FStar/blob/master/examples/dm4free/FStar.DM4F.Heap.ST.fst#L151 or here for a newer version: https://github.com/FStarLang/FStar/blob/c_erase_effect/examples/dm4free/FStar.DM4F.Heap.ST.fst#L169 Another thing I should mention is that effect aliases copy everything with the exception of the "totality" bit, which should explain the behavior you're seing above: you're basically creating FOO a divergent(!) variant of PURE ... exactly like we define DIV in our prelude. If you want a total effect you need to add the `total` keyword: total new_effect FOO = PURE 4. Is there an easy way to check consistency? Currently, I wrote a makefile > to test both validity and consistency (by appending an assert false at the > end) of a module (the MODS variable is the list of module names): > > >> $(addsuffix .fst.hints,$(MODS) $(addsuffix .False,$(MODS))): %.fst.hints: >> %.fst >> $(FSTAR) --record_hints $< > > > > $(addsuffix .valid,$(MODS)): %.valid: %.fst %.fst.hints >> $(FSTAR) --use_hints $< >> touch $@ > > > > $(addsuffix .False.fst,$(MODS)): %.False.fst: %.fst >> sed 's/^module $*/module $*.False/' $< > $@ >> echo >> $@ >> echo "let () = assert false" >> $@ > > > > $(addsuffix .consistent,$(MODS)): %.consistent: %.False.fst >> ! $(FSTAR) $< 2>/dev/null >> touch $@ > > I'm not aware of any better way of doing this. > 5. I read https://github.com/FStarLang/FStar/wiki/Dealing-with-F%E2% > 98%85-dependencies but I don't understand how dependencies work and what > they mean. It looks like verifying a module with fstar.exe MyModule.fst > does not generate any proof file (except the hints if asked). If module B > depends on module A, can I verify both in parallel? If I can't, then why > should they be verified in parallel? Verifying module B might use A hints? > The way we use parallelism at the moment is either more coarse grained than this, basically parallelizing the checking of multiple separate file in batch mode using a Makefile, or more fine grained by passing the experimental `--n_cores` to F* and sending off queries to multiple Z3 processes. Don't think we can currently parallelize a file's dependencies (beyond maybe --n_cores achieving a bit of that when you also pass --verify_all, since otherwise dependencies are anyway only lax type-checked). As for writing things to disk, there is an experimental feature that can be turned on with `--cache_checked_modules` but some of us have never been able to use it so far (https://github.com/FStarLang/FStar/issues/1213). Please note that these are just serializations of the elaborated terms, not proof terms like in Coq. F* doesn't have proof terms. Hope this helps, Catalin
_______________________________________________ fstar-club mailing list fstar-club@lists.gforge.inria.fr https://lists.gforge.inria.fr/mailman/listinfo/fstar-club
