Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Build F* with dune instead of ocamlbuild #2815

Merged
merged 151 commits into from
Feb 21, 2023
Merged

Build F* with dune instead of ocamlbuild #2815

Changes from 1 commit
Commits
Show all changes
151 commits
Select commit Hold shift + click to select a range
8a5e410
step 1: instructions for a dune snapshot for the compiler and minimal…
tahina-pro Jan 24, 2023
e0df548
snap
tahina-pro Jan 25, 2023
31182a0
step 2: compile F* with dune
tahina-pro Jan 25, 2023
840e677
escape hatch to not verify `experimental`
tahina-pro Jan 25, 2023
76b5fc2
generate a fstar-stdlib snapshot
tahina-pro Jan 25, 2023
1036be2
special treatment for FStar.Pervasives
tahina-pro Jan 25, 2023
8ac0fb8
extract fstar-stdlib (formerly fstarlib)
tahina-pro Jan 25, 2023
1291dfb
snap
tahina-pro Jan 25, 2023
b4f42ac
extract some taclib
tahina-pro Jan 25, 2023
6e61ddf
snap
tahina-pro Jan 25, 2023
cad908a
load new fstar.taclib
tahina-pro Jan 25, 2023
f46c04c
snap
tahina-pro Jan 25, 2023
988620f
always print dynlink error
tahina-pro Jan 26, 2023
3f5f331
use -linkall for fstar.exe
tahina-pro Jan 26, 2023
e92863c
stage dune snapshot build
tahina-pro Jan 26, 2023
69cb66c
snap
tahina-pro Jan 26, 2023
9a1c44e
build fstar and libs from the dune snapshot, and verify ulib
tahina-pro Jan 26, 2023
7821bcd
dune-full-bootstrap
tahina-pro Jan 26, 2023
e9e39b0
overwrite FStar_Version.ml, do not extend it
tahina-pro Jan 26, 2023
3c726c0
snap
tahina-pro Jan 26, 2023
301393b
make sure we are not using a stale F* snapshot
tahina-pro Jan 26, 2023
408c53d
restore automatic tactic plugin compilation
tahina-pro Jan 26, 2023
cbcefb8
snap
tahina-pro Jan 26, 2023
6a5859a
no need to dynlink taclib anymore!
tahina-pro Jan 26, 2023
f23810d
snap
tahina-pro Jan 26, 2023
da9ce82
dune-bootstrap
tahina-pro Jan 27, 2023
2c7f81f
merge all libs
tahina-pro Jan 27, 2023
9e748db
snap
tahina-pro Jan 27, 2023
21bfa07
move CI entrypoint to root makefile, prepare for dune CI
tahina-pro Jan 27, 2023
6dea28a
add an explicit ocamlbuild rule
tahina-pro Jan 27, 2023
7b4a0c9
use Dune
tahina-pro Jan 27, 2023
0b02e48
ToDocument: preserve state of unfold_tuples
tahina-pro Jan 28, 2023
113f430
snap
tahina-pro Jan 28, 2023
a1855b9
fstarlib -> fstar.lib
tahina-pro Jan 28, 2023
eb38a57
add handwritten Steel ml files
tahina-pro Jan 28, 2023
29b8519
snap
tahina-pro Jan 28, 2023
e75cf5b
Merge branch 'taramana_dune_step_1' into taramana_dune_step_2
tahina-pro Jan 28, 2023
1b70d53
ocamlc -> ocamlopt
tahina-pro Jan 28, 2023
44301e8
examples/semiring: fstar-tactics-lib -> fstar.lib
tahina-pro Jan 30, 2023
2219770
Merge branch 'master' of github.com:FStarLang/FStar into taramana_dun…
tahina-pro Jan 30, 2023
98b4c9f
snap
tahina-pro Jan 30, 2023
deed0c6
remove ocamlbuild snapshot
tahina-pro Jan 30, 2023
c3914d5
remove handwritten ulib files
tahina-pro Jan 30, 2023
6224933
remove handwritten ml files in src/
tahina-pro Jan 30, 2023
acca4e3
generate everything directly into the snapshot, remove everything abo…
tahina-pro Jan 31, 2023
0b39cd8
extract everything in parallel
tahina-pro Jan 31, 2023
52cf538
tidy use of DUNE_SNAPSHOT
tahina-pro Jan 31, 2023
014314d
define FSTAR_HOME in src/ocaml-output/Makefile
tahina-pro Jan 31, 2023
23028be
remove handwritten files from ulib/experimental/ml
tahina-pro Jan 31, 2023
4825a2c
verify ulib before extracting it
tahina-pro Jan 31, 2023
603f2b6
extraction: drop paths in ranges
mtzguido Jan 31, 2023
8607890
.gitignore: ignore lib/
mtzguido Jan 31, 2023
ba0ec5f
snap, for compiler sources
mtzguido Jan 31, 2023
6ddfc73
snap, second for ulib files containing ranges
mtzguido Jan 31, 2023
3b910e4
move FStar_Version from generated to dynamic
tahina-pro Feb 1, 2023
bf18af2
snap
tahina-pro Feb 1, 2023
61de305
CI: update snapshot diff check
tahina-pro Feb 1, 2023
23b74b5
fix FSTAR_HOME in src/ocaml-output/Makefile
tahina-pro Feb 1, 2023
4b1f0ec
Merge branch 'master' of github.com:FStarLang/FStar into taramana_dun…
tahina-pro Feb 1, 2023
02ba786
snap
tahina-pro Feb 1, 2023
39179b8
extraction: drop paths in ranges
mtzguido Jan 31, 2023
164b354
snap
tahina-pro Feb 1, 2023
193716f
remove old snapshot
tahina-pro Feb 1, 2023
f9f2d4e
Merge branch '_taramana_dune_merge' into _taramana_dune
tahina-pro Feb 1, 2023
35e5a7c
remove all mentions of "fstarlib, fstartaclib, fstar-tactics-lib"
tahina-pro Feb 1, 2023
9d323d7
snap
tahina-pro Feb 1, 2023
86819c6
FStar.Tactics.Load.load_lib, try_load_lib no longer needed
tahina-pro Feb 1, 2023
2dd9ab9
restore the boot rule
tahina-pro Feb 1, 2023
085483c
update the compilation instructions
tahina-pro Feb 1, 2023
87d073d
a top-level verify-ulib rule
tahina-pro Feb 1, 2023
b02a50d
document `make verify-ulib`
tahina-pro Feb 1, 2023
186f455
Merge branch 'master' of github.com:FStarLang/FStar into _taramana_du…
tahina-pro Feb 1, 2023
59f9513
snap
tahina-pro Feb 1, 2023
dbb3bab
remove ocamlbuild snapshot
tahina-pro Feb 1, 2023
fc769a4
Merge branch '_taramana_dune_merge' into _taramana_dune
tahina-pro Feb 1, 2023
7514956
Makefile: PWD -> CURDIR
tahina-pro Feb 2, 2023
05314a3
reinstate `make install`
tahina-pro Feb 2, 2023
230e9d6
eci19 does not need FSTAR_HOME
tahina-pro Feb 2, 2023
7f42b18
a Dockerfile to test `make package` without OCaml
tahina-pro Feb 2, 2023
2663ccb
.gitattributes: do not show diff in ocaml/fstar-lib/generated
mtzguido Feb 2, 2023
400f371
Makefiles: autogenerate FStar_Version.ml on each run, do not check it in
mtzguido Feb 2, 2023
c3a71a5
Makefile.boot: take tests out of the library
mtzguido Feb 3, 2023
90b24c5
dune: fstar-tests: add public name to obtain an executable
mtzguido Feb 2, 2023
12fd6f4
Makefile: restore unit tests on ci rule
mtzguido Feb 2, 2023
d64b62c
snap, test ml files move to fstar-tests/generated
mtzguido Feb 3, 2023
1937ace
clarify fstar.opam
tahina-pro Feb 2, 2023
c0864c8
fix multifile example
tahina-pro Feb 2, 2023
fc54eb0
fix installation of doc/tutorial
tahina-pro Feb 2, 2023
e134f6a
for parts that do not work outside of F* sources, remove them from in…
tahina-pro Feb 2, 2023
8f7e674
`opam remove` needs no explicit `make uninstall`
tahina-pro Feb 3, 2023
55fa49f
fix `make uninstall`
tahina-pro Feb 3, 2023
7231315
book: fstarlib -> fstar.lib
tahina-pro Feb 3, 2023
7d2500d
ulib vs. lib/fstar is independent of FSTAR_HOME
tahina-pro Feb 3, 2023
6c8c760
move FStar_Tests_ files to ocaml/fstar-tests/generated
tahina-pro Feb 3, 2023
1748089
Merge branch 'master' of github.com:FStarLang/FStar into _taramana_du…
tahina-pro Feb 3, 2023
2a4b448
snap
tahina-pro Feb 3, 2023
d4733bb
remove the OCaml snapshot
tahina-pro Feb 3, 2023
5aec95d
Merge branch '_taramana_dune_merge' into taramana_dune
tahina-pro Feb 3, 2023
2031bcb
move FStar_Version.ml from generated to dynamic
tahina-pro Feb 4, 2023
b160b43
Merge branch '_taramana_dune_step_2' into _taramana_dune
tahina-pro Feb 4, 2023
e2f334a
include extracted ulib/fs into binary package
tahina-pro Feb 6, 2023
e90266a
do not include the nuget package, but do include ulibfs.dll
tahina-pro Feb 6, 2023
7769171
ulib/Makefile.extract.fsharp: avoid long cmdline for dependency analysis
tahina-pro Feb 6, 2023
4eade93
extract ulibfs using existing checked, no need for lax
tahina-pro Feb 7, 2023
9654a0d
Merge branch 'master' of github.com:FStarLang/FStar into _taramana_du…
tahina-pro Feb 7, 2023
c7685de
Makefile: comment
mtzguido Feb 6, 2023
079babf
dune: silence warnings
mtzguido Feb 7, 2023
c75c3b1
Makefiles: tidy up info messages
mtzguido Feb 6, 2023
0b15d92
re-extract F* snapshot
tahina-pro Feb 7, 2023
d24c786
bump checked files version number
tahina-pro Feb 7, 2023
e9813c0
snap
tahina-pro Feb 7, 2023
5a5692d
remove old ocamlbuild snapshot
tahina-pro Feb 7, 2023
468f832
Merge branch '_taramana_dune_merge' into _taramana_dune
tahina-pro Feb 7, 2023
f37e300
Merge branch '_taramana_dune' of github.com:FStarLang/FStar into _tar…
tahina-pro Feb 7, 2023
f5b7eb5
update testing Dockerfiles
tahina-pro Feb 7, 2023
248ecda
fix the package build script
tahina-pro Feb 7, 2023
5d10f12
minimal restore of nix flake
tahina-pro Feb 8, 2023
6b8a190
nix flake: install everything
tahina-pro Feb 8, 2023
bc9bfa0
fulfill all actions of `dune install`
tahina-pro Feb 8, 2023
1f0c342
Merge branch 'master' of github.com:FStarLang/FStar into _taramana_du…
tahina-pro Feb 10, 2023
0ab6859
snap
tahina-pro Feb 10, 2023
225c59d
remove the ocamlbuild snapshot
tahina-pro Feb 10, 2023
6d5cf43
Merge branch '_taramana_dune_merge' into _taramana_dune
tahina-pro Feb 10, 2023
82d2e26
mlexpr_of_range: what if filename has no `/` ?
tahina-pro Feb 10, 2023
e957f44
snap
tahina-pro Feb 10, 2023
7a54d99
update the build process
pnmadelaine Feb 9, 2023
2cc1a6f
leverage the install-sides rule
tahina-pro Feb 10, 2023
8d1edab
`make -C src clean` shouldn't erase `generated/`
tahina-pro Feb 14, 2023
056150a
fix `make -C ulib clean`
tahina-pro Feb 14, 2023
7ea6196
more intermediate files to cleanup
tahina-pro Feb 14, 2023
0730555
clarify what to clean when in the root Makefile
tahina-pro Feb 14, 2023
0fb05c9
Merge branch 'master' of github.com:FStarLang/FStar into _taramana_du…
tahina-pro Feb 14, 2023
c222f0f
snap
tahina-pro Feb 14, 2023
c596682
remove ocamlbuild snapshot
tahina-pro Feb 14, 2023
08d68a5
Merge branch '_taramana_dune' into _taramana_dune_merge
tahina-pro Feb 14, 2023
8e35a31
Nix update
pnmadelaine Feb 12, 2023
5865554
tweaks to Makefiles
mtzguido Feb 14, 2023
cd076c6
/Makefile: tidy PHONY rules and reintroduce shortcuts
mtzguido Feb 14, 2023
571a668
snap
mtzguido Feb 14, 2023
d883f05
ocaml: .gitignore version.txt and silence copy rule
mtzguido Feb 14, 2023
7f99f6d
ocaml/dune: ignore all warnings
mtzguido Feb 14, 2023
7a914d7
`dune --prefix` does not support Cygwin paths
tahina-pro Feb 14, 2023
f1ca638
Merge remote-tracking branch 'pnm/dev' into _taramana_dune
tahina-pro Feb 14, 2023
c0a7927
Merge branch 'master' of github.com:FStarLang/FStar into _taramana_du…
tahina-pro Feb 14, 2023
a108445
explicitly call bash from dune when regenerating FStar_Version.ml
tahina-pro Feb 14, 2023
de65146
snap
tahina-pro Feb 14, 2023
a297ac5
remove ocamlbuild snapshot
tahina-pro Feb 14, 2023
e9a951e
Merge branch '_taramana_dune_merge' into _taramana_dune
tahina-pro Feb 14, 2023
d3e0aef
checkedfiles: suppress not found warning for --lax
mtzguido Feb 14, 2023
a7feb41
require dune >= 3.2.0
tahina-pro Feb 15, 2023
6a26ef0
Merge branch 'master' into _taramana_dune
tahina-pro Feb 21, 2023
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
15 changes: 14 additions & 1 deletion Makefile
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -1,4 +1,4 @@
.PHONY: all package clean boot 0 1 2 3 hints bench libs output install uninstall package_unknown_platform no-ulib-checked
.PHONY: all package clean boot 1 2 3 hints bench output install uninstall package_unknown_platform

include .common.mk

Expand Down Expand Up @@ -122,3 +122,16 @@ ci-uregressions:

ci-uregressions-ulong:
$(Q)+$(MAKE) -C src uregressions-ulong

# Shortcuts:

1: dune-fstar

2:
+$(MAKE) -C src ocaml
+$(MAKE) dune-fstar

3:
Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

FYI @nikswamy @aseemr, this is a way to bootstrap the compiler without verifying/extracting ulib. It won't work if something in ulib that the compiler depends on changed significantly, but it can save you time otherwise

+$(MAKE) dune-fstar
+$(MAKE) -C src ocaml
+$(MAKE) dune-fstar