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?
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.
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).
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 $@
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 the 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?
Thanks, (and sorry if the questions are stupid, I could not find an answer
by myself),
Julien
_______________________________________________
fstar-club mailing list
fstar-club@lists.gforge.inria.fr
https://lists.gforge.inria.fr/mailman/listinfo/fstar-club
