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.

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

Remove Steel from the F* code base #2889

Merged
merged 114 commits into from
May 3, 2023
Merged
Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
114 commits
Select commit Hold shift + click to select a range
4e0aabe
Karamel AST: add union and array types
tahina-pro Apr 12, 2023
a16763c
translate_type_without_decay; make C extraction modular
tahina-pro Apr 12, 2023
7ef4eab
use `let _ =`
tahina-pro Apr 12, 2023
38cef8c
snap
tahina-pro Apr 12, 2023
57e1ab8
also make translate_let extensible
tahina-pro Apr 12, 2023
b012c90
Revert "snap"
tahina-pro Apr 12, 2023
17acd9e
snap
tahina-pro Apr 12, 2023
92b495c
Revert "snap"
tahina-pro Apr 12, 2023
e0a4da8
split off the Steel extraction rules
tahina-pro Apr 12, 2023
52183ff
snap
tahina-pro Apr 12, 2023
c83d43d
remove Steel
tahina-pro Apr 13, 2023
ef6288a
set some compatibility flag for FStar.NMST
tahina-pro Apr 13, 2023
76a7d0a
snap
tahina-pro Apr 13, 2023
1376c61
(TEMP) use Karamel _taramana_no_steel
tahina-pro Apr 13, 2023
1215aad
Steel bug report 2605 moved away
tahina-pro Apr 13, 2023
8d066f6
doc: disable ContextPollution
tahina-pro Apr 13, 2023
28ad84f
make FStar.Parser.Dep.core_modules a function
tahina-pro Apr 13, 2023
847b5b7
Revert "snap"
tahina-pro Apr 13, 2023
a8704c8
snap
tahina-pro Apr 13, 2023
bbbb9f0
Revert "(TEMP) use Karamel _taramana_no_steel"
tahina-pro Apr 13, 2023
afde4ee
(TEMP) use Karamel taramana_no_steel
tahina-pro Apr 13, 2023
df704e3
Merge branch 'master' of github.com:FStarLang/FStar into taramana_no_…
tahina-pro Apr 13, 2023
55ada1b
remove Pulse
tahina-pro Apr 15, 2023
cd951dc
remove Steel
tahina-pro Apr 15, 2023
dc98a9d
Merge branch 'taramana_no_steel_merge_20230414' into taramana_no_steel
tahina-pro Apr 15, 2023
d2376f9
advance F* version number to 2023.04.15
tahina-pro Apr 15, 2023
c9cd885
Merge branch 'master' of github.com:FStarLang/FStar into taramana_no_…
tahina-pro Apr 18, 2023
1188f38
two new reflection primitives: range_of_term and range_of_sigelt
nikswamy Apr 19, 2023
7cb2ee5
remove Pulse
tahina-pro Apr 20, 2023
69b49e5
Merge branch 'merge_20230419' into taramana_no_steel
tahina-pro Apr 20, 2023
55d5eb2
more range utilities in reflection and tactics
nikswamy Apr 20, 2023
921dd41
merging in guido_range
nikswamy Apr 20, 2023
44e3347
bootstrap
nikswamy Apr 21, 2023
8efed96
remove Steel and Pulse
tahina-pro Apr 21, 2023
24ed334
partially revert a8704c88f3adb6e87b1d6f6d4c88c6f287c22367
tahina-pro Apr 21, 2023
2c866d8
Merge branch 'merge_20230420' into taramana_no_steel
tahina-pro Apr 21, 2023
ff6cdf4
snap
tahina-pro Apr 21, 2023
d36f875
merging master in
aseemr Apr 21, 2023
b419530
Merge branch 'taramana_no_steel' of github:FStarLang/FStar into guido…
mtzguido Apr 21, 2023
20039e9
Merge pull request #2884 from FStarLang/guido_range
nikswamy Apr 21, 2023
3b18d53
Merge branch 'master' into taramana_no_steel
aseemr Apr 24, 2023
f489d54
basic: split GenSym into own module
mtzguido Apr 24, 2023
f5813e6
nits on Makefile
mtzguido Apr 24, 2023
64c256b
run_benchmark: update
mtzguido Apr 24, 2023
7688624
syntax: visit: nits
mtzguido Apr 24, 2023
c7a1060
tc: rel: small fix, freshen+open required
mtzguido Apr 24, 2023
e325c72
snap
mtzguido Apr 24, 2023
36e8bdf
examples: removing some old, time-consuming examples from CI
mtzguido Apr 24, 2023
daffd96
ulib: simplify extraction makefiles, add depgraph rule
mtzguido Apr 24, 2023
ef724cf
Makefile.arraystruct: remove stale Makefile
mtzguido Apr 24, 2023
ffdfc27
gen_mllib: remove now unneeded script
mtzguido Apr 24, 2023
961ce10
ulib: ml: Makefile nit
mtzguido Apr 24, 2023
9d98ab0
snap
mtzguido Apr 24, 2023
38e77ee
merging in taramana_no_steel
nikswamy Apr 25, 2023
b2fdb81
Merge pull request #2887 from FStarLang/nik_range_of_term
nikswamy Apr 25, 2023
912920f
[CI] regenerate hints + ocaml snapshot
Apr 25, 2023
d202003
[CI] bump version number to 2023.04.25~dev
Apr 25, 2023
4e8f5d1
Merge pull request #2888 from FStarLang/_BuildHints-_release
tahina-pro Apr 25, 2023
3baeb5d
Revert "[CI] bump version number to 2023.04.25~dev"
tahina-pro Apr 25, 2023
6c66ddc
remove Steel and Pulse hints
tahina-pro Apr 25, 2023
757853e
revert conflicting hint
tahina-pro Apr 25, 2023
30776e2
Merge branch '_release_merge_20230425' into taramana_no_steel
tahina-pro Apr 25, 2023
5ee8f31
bump version number to 2023.04.26~dev
tahina-pro Apr 25, 2023
b0bc6c8
(TEMP) CI: ignore branch taramana_no_steel
tahina-pro Apr 25, 2023
fd4a8e1
Merge branch 'guido_range' of github:FStarLang/FStar
mtzguido Apr 26, 2023
0828cf5
tosyntax: propagate sigelt attributes to each letbinding
mtzguido Apr 27, 2023
f9b9833
tc: keep attributes from original letbindings even when there is a val
mtzguido Apr 27, 2023
e646106
introduce an `admit_termination` attribute
mtzguido Apr 27, 2023
6267638
tests: add a test for @@admit_termination
mtzguido Apr 27, 2023
ab74f5c
tc: change the effect annotation for Sig_let
mtzguido Apr 27, 2023
364cbcd
snap
mtzguido Apr 27, 2023
6c6536c
update test
mtzguido Apr 27, 2023
53197a7
ulib: starting a userland verified term_eq
mtzguido Apr 26, 2023
ef72680
ulib: termeq: more cases
mtzguido Apr 27, 2023
f89ee53
Merge pull request #2896 from FStarLang/guido_misc
mtzguido Apr 27, 2023
e509dad
Revert "(TEMP) CI: ignore branch taramana_no_steel"
tahina-pro Apr 27, 2023
c375e11
snap
mtzguido Apr 27, 2023
e38c34e
examples: dsl: update
mtzguido Apr 27, 2023
d53e606
reflection: no BV sorts
mtzguido Apr 27, 2023
f4a26d0
snap
mtzguido Apr 27, 2023
a439964
tests: tactics: update for no bv sort
mtzguido Apr 27, 2023
6d8688e
WIP disable param
mtzguido Apr 28, 2023
ab9c201
tactics: make fresh_bv not take a type arg
mtzguido Apr 27, 2023
07b677a
nits
aseemr Apr 28, 2023
2f25008
proof for open_with_gt_ln
aseemr Apr 28, 2023
d8aff98
proof for equiv_abs_close
aseemr Apr 28, 2023
9957c4f
Merge branch 'taramana_no_steel' into _aseem_taramana_no_steel
aseemr Apr 28, 2023
01093d5
snap
aseemr Apr 28, 2023
fd1d643
fix examples
mtzguido Apr 28, 2023
68bd6f2
Merge branch 'taramana_no_steel' of github:FStarLang/FStar into dsl
mtzguido Apr 28, 2023
94d5280
syntax: print: a fix for vale
mtzguido May 1, 2023
eded8f3
snap
mtzguido May 1, 2023
d9bd7e4
syntax: print: a fix for vale
mtzguido May 1, 2023
394df67
snap
mtzguido May 1, 2023
9d18913
wip, adding ghost effect to reflection typing
aseemr May 2, 2023
4f273df
fixes in FStar.Reflection.Typing.fst
aseemr May 2, 2023
213d528
effect label type on the src side
aseemr May 2, 2023
549eac3
snap
aseemr May 2, 2023
3208686
embeddings for effect_label
aseemr May 2, 2023
c199b0d
snap
aseemr May 2, 2023
8dfd318
fixes to meta APIs to take effect label
aseemr May 2, 2023
db127ec
snap
aseemr May 2, 2023
37130b6
Merge branch 'taramana_no_steel' of github.com:FStarLang/FStar into g…
mtzguido May 2, 2023
f9dd78f
Merge branch 'master' of github.com:FStarLang/FStar into guido_no_steel
mtzguido May 2, 2023
d3a96af
abbreviations for tot and ghost typing
aseemr May 3, 2023
404adea
snap
aseemr May 3, 2023
e83bfb1
some nits to reflection typing
aseemr May 3, 2023
36a6c0f
changing effect_label to tot_or_gtot
aseemr May 3, 2023
4734327
snap
aseemr May 3, 2023
312a052
snap
aseemr May 3, 2023
e75e3ee
Merge branch 'master' into taramana_no_steel
aseemr May 3, 2023
e21853d
Merge branch 'taramana_no_steel' into aseem_ghost_reflection
aseemr May 3, 2023
bde73ec
fixing other dsls
aseemr May 3, 2023
4ab5019
Revert "(TEMP) use Karamel taramana_no_steel"
mtzguido May 3, 2023
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
The table of contents is too big for display.
Diff view
Diff view
  •  
  •  
  •  
1 change: 0 additions & 1 deletion .gitignore
Original file line number Diff line number Diff line change
Expand Up @@ -41,7 +41,6 @@ tests/*/*.ml
tests/incl/*.neg/error.log

_build/
/ulib/ml/_taclib_build/
/ulib/fs/obj
/ulib/fs/bin

Expand Down
18 changes: 10 additions & 8 deletions bin/run_benchmark.sh
Original file line number Diff line number Diff line change
Expand Up @@ -146,16 +146,16 @@ function clean_slate () {
# build fstar compiler bootstrap
T0=`date +'%Y%m%d_%H%M%S'`
echo "Starting fstar compiler bootstrap ${T0}"
make -j${JLEVEL} -C src ocaml-fstar-ocaml 2>&1 | tee ${BENCH_OUTDIR}/build_fstar.log
make -j${JLEVEL} dune-full-bootstrap 2>&1 | tee ${BENCH_OUTDIR}/build_fstar.log
T1=`date +'%Y%m%d_%H%M%S'`
echo "Finished fstar compiler boostrap ${T1} (started at ${T0})"

# verify ulib and install
# build library
T0=`date +'%Y%m%d_%H%M%S'`
echo "Starting fstarlib build ${T0}"
make -j${JLEVEL} -C src .fstarlib 2>&1 | tee ${BENCH_OUTDIR}/build_fstarlib.log
echo "Starting library build ${T0}"
make -j${JLEVEL} 2>&1 | tee ${BENCH_OUTDIR}/build_fstarlib.log
T1=`date +'%Y%m%d_%H%M%S'`
echo "Finished fstar compiler boostrap ${T1} (started at ${T0})"
echo "Finished library build ${T1} (started at ${T0})"

ls -ltr ulib >> ${BENCH_OUTDIR}/build_fstarlib.log
}
Expand All @@ -171,7 +171,8 @@ function bench_dir () {
# Remove old .bench files
find "${BENCH_DIR}" -name '*.bench' -delete

${BENCH_WRAP} make -j${JLEVEL} -C "${BENCH_DIR}" "${RULE}" BENCHMARK_CMD=orun OTHERFLAGS="${BENCH_OTHERFLAGS}" 2>&1 | tee ${BENCH_OUTDIR}/${NAME}.log
# We explicitly add -f since we have previously built F* and its library, we are re-checking here.
${BENCH_WRAP} make -j${JLEVEL} -C "${BENCH_DIR}" "${RULE}" BENCHMARK_CMD=orun OTHERFLAGS="${BENCH_OTHERFLAGS} -f" 2>&1 | tee ${BENCH_OUTDIR}/${NAME}.log
fi

cat_benches_into "${BENCH_DIR}" "${BENCH_OUTDIR}/${NAME}.bench"
Expand Down Expand Up @@ -380,9 +381,10 @@ check_for jq "Try to install it via your package manager, or see https://stedola

check_for orun "\
To install a local pinned copy of orun do the following:
$ git clone https://github.com/ocaml-bench/sandmark.git sandmark
$ git clone https://github.com/ocaml-bench/orun.git sandmark
$ cd sandmark/orun
$ opam install ."
$ opam install .
You may need to install libdw-dev via your package manager before."

# Second pass for options, only handles --custom which needs to run after the others
OPTIONS=
Expand Down
18 changes: 9 additions & 9 deletions doc/book/code/AdHocEffectPolymorphism.fst.hints

Some generated files are not rendered by default. Learn more about how customized files appear on GitHub.

28 changes: 14 additions & 14 deletions doc/book/code/Alex.fst.hints

Some generated files are not rendered by default. Learn more about how customized files appear on GitHub.

14 changes: 7 additions & 7 deletions doc/book/code/AlexOpaque.fst.hints

Some generated files are not rendered by default. Learn more about how customized files appear on GitHub.

Loading