Consider dropping requirement that F* code has to be valid F#

[catalin-hritcu]

We recently had a Slack discussion on the pros and cons of dropping the current requirement that the code of F* has to be valid F#. Fortunately, I saved this right before it went dodo.

@nikswamy @aseemr @protz @tahina-pro @mtzguido: Let's continue any discussions on this by commenting on this issue!

[A-Manning]

- 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

This is fairly easy to fix, most of the package issues regarding FSharp.Core etc. can be solved by using a tool like paket to handle dependencies. I'd be happy to contribute this myself, I wasn't aware that this was such a bothersome issue.

- 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

The build system is somewhat arcane either way - I don't have a good enough understanding of it to be able to contribute something alone, but F# has sophisticated tooling for build automation (eg. FAKE(https://fake.build/), ProjectScaffold(http://fsprojects.github.io/ProjectScaffold/), which might be worth migrating to, considering the current complexity of the build process.

- 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

It probably wouldn't be too much effort to create a tool that could warn about this, and have it run as part of the build process. I'm skeptical of how much of a bother this part really is though - it's common for larger projects to have a strict code style, and it's not much trouble to get used to working in this subset, even without a specification of the subset.

- 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

It's unfortunate to have to take language design decisions to retain compatibility with F#'s syntax - especially regarding things like namespaces, which F* generally handles a lot better IMO. For example, F# can't handle FStar.Pervasives and FStar.Pervasives.Native in different files - whilst this is somewhat annoying when trying to get extracted F* to work with F#, I think it's a worthwhile annoyance if F* gets a better namespace mechanism out of it.
Some things like 'a syntax could probably be handled by a preprocessor. I think that's a worthwhile trade-off to not clutter F*'s syntax. I've never found 'a to be of much use in F* anyway.

Regarding F# compatibility, we depend heavily on being able to extract F# code and using the parser & prettyprinting components directly from F#. That said, having the sources written in the intersection of F#/F* isn't so important to us as long as we end up with dlls and a cross-platform executable. It is important that we are able to modify and test things quickly though, which includes changes to syntax, so even a bootstrapped approach might not be suitable.

[artagnon]

In developing #1742, I encountered many nasty corners — the subset of F# that I was supposed to be writing is not documented at all! I had to edit NotFStar.Util.fs in the process, and found that implementing nread in "F# with OCaml compatibility" was a pain — the CI runs the fstar-in-fsharp target, which I think is unnecessary in the long run. There were numerous compile errors that weren't caught at the source level, and only caught after the OCaml extraction finished; these were very painful to debug — one of the primary issues is that I had to duplicate all types written in the .fsi in the .fs as well; code duplication makes coding highly error-prone. Finally, there were runtime crashes because there's no way to tell if I'm exhaustively catching all exceptions — I think runtime crashes are unacceptable in a modern programming language.

Incidentally, many of @aseemr's woes from the Slack discussion will be over when the long tail of #1742 is finished — working with zero editor support can lead to many wasted cycles during development; that's the motivation to develop fstar.exe --lsp in the first place. The first steps in the roadmap I propose are the following:

1. Get full editor support for .fs, .fsi, .fst, .fsti files from vsfstar and fstar.exe --lsp, but no theorem proving support at this stage. Develop it with first-class support for FStar.git.
2. Write a tiny amount of code (comparable to the volume of code in vsfstar) for all editors used by the development community to use fstar.exe --lsp, and get everyone fully migrated so nobody misses VS. For pure F* code, fstar-mode is still the best option at this stage.
3. Get the CI to drop the fstar-in-fsharp target; people can still use it locally at this stage.
4. Start converting code from F# to F* proper, and clean up F#'isms.

[artagnon]

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

The relevant lines from src/Makefile are:

fsharp-build-and-test:
        +$(MAKE) fstar-in-fsharp
        +$(MAKE) fsharp-unit-tests

# The first tests have to be performed sequentially (but each one may use some parallelism)
# Adding the F# build and F# tests also here
#   since in the uregressions target it may not be a good idea to override the fstar.exe binary?
utest-prelude: fsharp-build-and-test
        +$(MAKE) boot-ocaml        #build the ocaml-snapshot
        +$(MAKE) clean_extracted   #ensures that there is no leftover from previous extraction
        +$(MAKE) fstar-ocaml       #extract the compiler again and build the result
        +$(MAKE) ocaml-unit-tests  #run the unit tests
        +$(MAKE) fstarlib

[aseemr]

Ping. I implemented support for typechecking F* source files in emacs (using makefiles) and have been exclusively using it for past 3 months. It provides symbol lookup etc. and is good enough for me. With incremental bootstrapping support, I also don't rely on F# builds for quick testing anymore.

Happy to revive this discussion (and see if we want to decide either ways for v1).

[msprotz]

I remember there was a conclusion reached during one of the F* meetings. Can an update be posted here?

[nikswamy]

Transcribing a slack discussion here:

@aseemr wrote:

• On F# and F* intersection for the typechecker source, it seems that no one is using VS for F* development anymore so that constraint is gone. And with bootstrapping being incremental, it doesn't look like a big problem to bootstrap and test changes (than doing it in F#). That leaves the issue of staging some changes like to the parsers, we agreed that these changes are not as common. So, are we ready to leave behind this restriction of being in both F# and F*?

@nikswamy wrote:
on F# dependence: I'm also in favor of leaving it behind. But, it would be great if we could restore F# extraction before we do. Otherwise, there are people using F* on .NET who would be abandoned

I think there are people who use F* today without any dependence on OCaml, e.g., just by building the sources in F#. If we still want to support that, then we need a way to produce an fsharp-snapshot of the compiler

@aseemr:
it seems important to me (to continue supporting such users)

@protz
it seems that people who use the F# build of F* are on windows, correct? for those users, wouldn't a binary package be equally well suited?

@nikswamy
yes, a binary package would work ... but then we should get good about producing binaries regularly. not sure what the status of our nightly builds are

@catalin-hritcu
they seem to be working fine since our last release (which seems like a record)

@nikswamy
nice

---

Separately, I recall us discussing that we should post prominently here, on the mailing list, on zulip and slack, indicating that we are considering leaving behind the ability to build the F* sources in F# and to see if there are any users out there who are relying on this feature in some way that we have not anticipated.

For starters, @A-Manning, what do you think about this?

[A-Manning]

I think there are people who use F* today without any dependence on OCaml, e.g., just by building the sources in F#.

I wouldn't want to lose the ability to compile the F* sources as F#. It's really helpful for projects that use F* from F* - for example, I often use FStar.Parser and FStar.Pprint from F# to generate F* files. Migrating to OCaml would not be practical, unfortunately.

it seems that people who use the F# build of F* are on windows, correct? for those users, wouldn't a binary package be equally well suited?

There are quite a few of us using the F# build on Linux/OSX, and a binary would not be well-suited to those that have F* as a dependency.

[aseemr]

Done as part of #2512.