gistfile1.txt

catalin   [Mar 27th at 8:22 PM]
Noob question of the day. Can we fix `make -C examples/hello fs`? (It's our simple example of how to extract things to F# and run them.)
https://fstar.zulipchat.com/#narrow/stream/184683-questions-and.20help/topic/Compiling.20to.20F.23 (edited)
51 replies

nik   [1 month ago]
Not really an answer to your question, but somewhat related

nik   [1 month ago]
I was thinking last night while trying to debug stuff related to a nasty performance problem that the F# build of fstar.exe is really not providing me with that much value.

nik   [1 month ago]
my main use case for using the F# build of fstar was to use the VS debugger

nik   [1 month ago]
but the VS 2017 debugger often crashes for me randomly in the middle of a debugging run

nik   [1 month ago]
i can't remember the last time i've used it successfully

nik   [1 month ago]
this is controversial, but I wonder if we should finally just give up on the sources of F* being in the shared subset of F* and F#

nik   [1 month ago]
that would free us up to do many things that we can't do now (e.g., verify parts of the compiler, use nice printf notations, etc)

catalin   [1 month ago]
is bootstrapping via an old OCaml version guaranteed to always work?

nik   [1 month ago]
and, coming finally to Catalin's question, we could extract the source to F# to produce an fstar.exe for .net/mono

nik   [1 month ago]
that would also help us make sure that the F# extraction doesn't bitrot

nik   [1 month ago]
breaking the overlap of F* and F# does have some costs

nik   [1 month ago]
- Not using VS for editing (I think Aseem and I still do that from time to time)

catalin   [1 month ago]
(me too, but very rarely these days)

nik   [1 month ago]
- Ensuring that the ocaml snapshot is always capabale of bootstrapping the sources (it's possible to ensure this, I think ... but some changes would have to be staged. E.g., you can't just change the parser and start to use new syntax in the source code and hope to bootstrap with an old snapshot)

nik   [1 month ago]
- Longer build cycles for basic development ... you can't just do a quick test in F#, you have to bootstrap

nik   [1 month ago]
Anyway, probably others that I am forgetting

nik   [1 month ago]
I'm not advocating for this to change immediately, but I think it's worth discussing

nik   [1 month ago]
@aseem @guido @protz et al

protz   [1 month ago]
I will personally bring a bottle of fine French liquor if we drop the F# restriction!

taramana   [1 month ago]
it sounds like the Communist party giving up on Marxism...

taramana   [1 month ago]
all jokes aside, we might mind the people working on Windows, for whom installing OCaml might be more painful than installing F#, and so those people might prefer relying on a F#-based F* than an OCaml-based one

nik   [1 month ago]
we could retain both an ocaml-snapshot and an fsharp-snapshot for that scenario

nik   [1 month ago]
@taramana Permanent revolution!

aseem   [1 month ago]
For me it would be a *huge* inconvenience to break the overlap betweek F* and F# for the compiler, for the reasons Nik already listed

aseem   [1 month ago]
I still use VS to edit the compiler code almost all the time

aseem   [1 month ago]
Being able to compile using F# is also very handy and I use it when some change has broken bootstrapping, this way I don't have to think about bootstrapping just to finish the change in question

nik   [1 month ago]
What VS features do you rely on the most? "Find all references?" I find that that has become unreliable in VS2017, so I end up doing `git grep`

nik   [1 month ago]
I wonder what it would take to set of %.fst-in targets for the F* compiler files and just use fstar-mode.el for them

nik   [1 month ago]
anyhow, I totally hear you that this change would be a big inconvenience

nik   [1 month ago]
So, open to any other ideas too ... ultimately, we need a way forward if we ever want to say, apply some lightweight formal verification to the compiler itself

aseem   [1 month ago]
None of the reasons I listed are un-doable, it could just be changing the habits which can be done if push comes to shove (edited)

aseem   [1 month ago]
I also use jump to definitions, which can be done in emacs with F* running the background

aseem   [1 month ago]
Yeah, show all references is a bit unreliable these days

aseem   [1 month ago]
Type checking in VS also helps, that's the first level of typechecking that I rely on before bootstrapping (edited)

catalin   [1 month ago]
Could we change to bootstrapping via Ocaml snapshot for a couple of months and make sure that works before doing any irreversible switch?

catalin   [1 month ago]
So no green unless it can be bootstrapped via OCaml snapshot, basically simulating the process we will be forced to use without F#

aseem   [1 month ago]
F* CI build already bootstraps the compiler using the checked-in OCaml snapshot (edited)

guido   [1 month ago]
I haven't been using the F# build for a long time, but I also don't really mind staying in the intersection

protz   [1 month ago]
Another point of view to consider, beyond the seasoned F* hackers who have internalized all the restrictions, is that of newcomers; people interested in contributing code to the F* compiler; people who hack on lower-level bits of the compiler.

Keeping the F# \cap F* intersection constraint means:
- all the low-level bits of the compiler (e.g. z3 process management & interrupts, interaction with the filesystem, etc.) have to be done twice; this is an area where we oftentimes need help, and we're adding much more than 2x the normal burden to would-be contributors, since in addition to doing the work twice, one needs to ensure the behaviors are the same
- semantics differences: Nik wasted a bunch of cycles debugging a global initialization issue where the semantics differed between F# and OCaml; the parser is not the same in spite of our efforts; so really there's two versions of F* that behave differently and we're burning precious developer time dealing with those
- lexer burden: the lexer, which is another low-level area where we desperately need help (e.g. fsdoc), is duplicated and exists twice, meaning anyone attempting to make things better has to do it twice, or acknowledge that it'll only work well in OCaml, not F#; as an example, consider that the recent F* change for reals exhibited syntax differences between F# and OCaml in the first version of the pull request (we've had rampant issues with machine integers, too)
- parser complexity: the parser dance going through ocamlyacc then fsyacc only exists because of the F# constraint (I think)
- build complexity: we have two maintain two build systems; I seem to recall the F# build has more constraints re. the dependencies across sub-projects
- version complexity: we regularly waste cycles trying to figure out which package we should require so that the F# build works on mono, VS2017, VS2015... as far as I know, we haven't had comparable difficulties with OCaml
- syntactic restrictions: there's a magic subset of F# and F* that is unspecified; whether you write F# or F* first, you're bound to be bitten by the other build once you need to debug your code -- I understand and appreciate that it's easy to internalize and forget once you hack on the F* compiler on a regular basis, but for people who are would-be contributors or occasional contributors, it might not be that natural to write in that subset
- hacks all over the place: // ONLY FSHARP, etc. have pervaded the source code; some are hardcoded into the lexer; it's a lot of effort that we have to maintain; sed rules in the build (do we still have those?)
- some language design decisions were informed by the need to retain compatibility with F#: 'a notation for type variables, but also namespace resolution rules, which in turn made dependency analysis and name resolution more difficult, with numerous iterations by e.g. Tahina to get it right -- I *seem* to recall (but correct me if I'm wrong!) that one reason why we can't have a lexing-only dependency analysis is because we chose to retain the same behavior as F# re. the current namespace
- the cost goes beyond the F* compiler itself: in ulib, if you happen to modify a file that's reachable via the compiler (e.g. FStar.List), then you get build errors because the file is interpreted once with Tot as the default effect and once more with ML as the default effect; these are hidden, undocumented semantics that add up and make not just hacking on the compiler more difficult, but hacking on ulib itself more difficult; if we got rid of F#, we could annotate once and for all all the definitions in the compiler with the ML effect, and get rid of this behavior

I think we should fight inertia and seriously consider dropping the F# dependency. This is only a subset of the consequences of retaining F# compatibility: I remember other discussions where the conclusion was "we can't fix this language feature because of F# compatibility" but I can't remember what they were about.

protz   [1 month ago]
I remember discussions about this in private with @kyod and I also remember that @cpitclaudel was keen to make fstar-mode work well with the F* compiler; they may have thoughts on the matter too

nik   [1 month ago]
Thanks for those points @protz. I agree with most of them. However, many of them would still be an issue if we left the F# \cap F* restriction behind. In particular, I would still want to produce a .NET version of fstar.exe, requiring F# versions of all support libraries, lexers, parsers etc (edited)

nik   [1 month ago]
Leaving F# behind altogether would upset a lot of people who are using F* with F#. E.g., Zen

nik   [1 month ago]
Especially as OCaml for windows still really doesn't work out of the box (cygwin etc.)

protz   [1 month ago]
yes, if we want to retain the ability to distribute an F# version of F*, some of these points are moot (edited)

nik   [1 month ago]
As for the `JUST FSHARP` hacks. I don't think it's fair to blame F#. It's more the fault of F* type inference. There are 18 of these hacks in the compiler, most of them very similar to each other. E.g.,
```// IN F*: let rec e_tactic_thunk (#r:Type) (er : embedding r) : embedding (tac r)
let rec e_tactic_thunk (er : embedding<'r>) : embedding<(tac<'r>)> // JUST FSHARP```
That `JUST FSHARP` line should just work in F* too, but we hit some bug that I haven't bothered to fix. So better to blame me for them than F#.

aseem   [1 month ago]
Thanks Jonathan, like Nik I also agree with many of them ... in addition to the points above, the `FStar.List` kind of problems would also remain, since it requires `Tot` annotations in the list library. That seems independent of F# (at least that's how I understand this issue)

aseem   [1 month ago]
I would be happy to start using emacs for compiler hacking too so as to get used to it. Curious to know how @nik and @guido do it, do you have an F* process running for querying symbol type, jump to definition etc.?

guido   [1 month ago]
I mostly go commando using vim+git+grep+others. If the interactive mode worked I'd definitely try it, but I probably won't fully switch

nik   [1 month ago]
I also just use emacs with git+grep ... but it shouldn't be so hard to set up fstar-mode on compiler files

nik   [1 month ago]
in fact, I think fstar-mode has some specialized support for editing compiler files ... though I've never really gotten that to work well

nik   [1 month ago]
i think it would be easy to configure fstar-subp-prover args to work for compiler files