catalin-hritcu
commented
7 years ago I'm continuing the cleanup Nik started and will remove most directories in examples that are not in any Makefile. Here is what removed tonight (last version including these things a21e94b9, actual remove was 26d426f8a):
asm: never in Makefile, obsolete since 2016-02, doesn't work, nontrivial fix
contributor: Nik Swamy
circuitcompiler: never in Makefile, obsolete since 2016-03, never worked
contributor: Michael Lowell Roberts
deriving-monads: obsolete since 2016-07, leftover of DM4F, safe to remove
contributor: Aseem Rastogi
jsbackend: dead, `polubelova_backends` branch can bring it back
low-star: dead (JK)
machine_integers: dead (JK)
monads: might still want to bring back EtherST at some point?
the rest is a dead experiment
contributor: Nik Swamy (EtherST), Catalin (rest)
primitives: interesting but needs some porting work, might also move to hacl*
contributor: Jean Karim
sgx: will need to bring back when it's ready
contributors: Anitha Gollamudi, Aseem Rastogi
test: dead, obsolete since 2016-03 (Nik Swamy)Or in more detail
[hritcu@detained examples]$ git rm -r asm (git)-[catalin_private]
rm 'examples/asm/asm.fst'
[hritcu@detained examples]$ git rm -r circuitcompiler (git)-[catalin_private]
rm 'examples/circuitcompiler/Makefile'
rm 'examples/circuitcompiler/arithcircuit.fst'
rm 'examples/circuitcompiler/ast.fst'
rm 'examples/circuitcompiler/circuitlib.fst'
rm 'examples/circuitcompiler/cktast.fst'
rm 'examples/circuitcompiler/fixnat.fst'
rm 'examples/circuitcompiler/gckct.fst'
rm 'examples/circuitcompiler/gencircuit.fst'
rm 'examples/circuitcompiler/mylist.fst'
rm 'examples/circuitcompiler/newlist.fst'
rm 'examples/circuitcompiler/wires.fst'
[hritcu@detained examples]$ git rm -r deriving-monads (git)-[catalin_private]
rm 'examples/deriving-monads/exn.fst'
rm 'examples/deriving-monads/st.fst'
[hritcu@detained examples]$ git rm jsbackend (git)-[catalin_private]
fatal: not removing 'jsbackend' recursively without -r
[hritcu@detained examples]$ git rm -r jsbackend (git)-[catalin_private]
rm 'examples/jsbackend/Makefile'
rm 'examples/jsbackend/constants.fst'
rm 'examples/jsbackend/fun.fst'
rm 'examples/jsbackend/lib/stdlib.js'
rm 'examples/jsbackend/record.fst'
rm 'examples/jsbackend/strings.fst'
rm 'examples/jsbackend/tuples.fst'
[hritcu@detained examples]$ git rm -r low-star (git)-[catalin_private]
rm 'examples/low-star/Makefile'
rm 'examples/low-star/buffer.fst'
rm 'examples/low-star/demo.fst'
rm 'examples/low-star/file1.txt'
rm 'examples/low-star/file2.txt'
rm 'examples/low-star/header.txt'
rm 'examples/low-star/lsarray.fst'
rm 'examples/low-star/ml/CBuffer.ml'
rm 'examples/low-star/ml/CSystem.ml'
rm 'examples/low-star/ml/Test.ml'
rm 'examples/low-star/ml/cfun.c'
rm 'examples/low-star/source.fst'
rm 'examples/low-star/system.fst'
rm 'examples/low-star/target.c'
rm 'examples/low-star/target.fst'
[hritcu@detained examples]$ git rm -r machine_integers (git)-[catalin_private]
rm 'examples/machine_integers/FStar.MachineArray.fst'
rm 'examples/machine_integers/Makefile'
rm 'examples/machine_integers/test.ml'
[hritcu@detained examples]$ git rm -r monads (git)-[catalin_private]
rm 'examples/monads/etherst.fst'
rm 'examples/monads/pure.fst'
rm 'examples/monads/pure2.fst'
[hritcu@detained examples]$ git rm -r primitives (git)-[catalin_private]
rm 'examples/primitives/.gitignore'
rm 'examples/primitives/Bignum.Bigint.fst'
rm 'examples/primitives/Bignum.Core.fst'
rm 'examples/primitives/Bignum.Fdifference.fst'
rm 'examples/primitives/Bignum.FdifferenceLemmas.fst'
rm 'examples/primitives/Bignum.Fproduct.fst'
rm 'examples/primitives/Bignum.Fscalar.fst'
rm 'examples/primitives/Bignum.Fsum.fst'
rm 'examples/primitives/Bignum.FsumWide.fst'
rm 'examples/primitives/Bignum.Modulo.fst'
rm 'examples/primitives/Bignum.Parameters.fst'
rm 'examples/primitives/Crypto.AES.fst'
rm 'examples/primitives/Curve.AddAndDouble.fst'
rm 'examples/primitives/Curve.Ladder.fst'
rm 'examples/primitives/Curve.Point.fst'
rm 'examples/primitives/IntLibLemmas.fst'
rm 'examples/primitives/Makefile'
rm 'examples/primitives/README_POLY.txt'
rm 'examples/primitives/SBytes.fst'
rm 'examples/primitives/SInt.Cast.fst'
rm 'examples/primitives/SInt.UInt128.fst'
rm 'examples/primitives/SInt.UInt32.fst'
rm 'examples/primitives/SInt.UInt63.fst'
rm 'examples/primitives/SInt.UInt64.fst'
rm 'examples/primitives/SInt.UInt8.fst'
rm 'examples/primitives/TODO'
rm 'examples/primitives/axioms.fst'
rm 'examples/primitives/bigint.fst'
rm 'examples/primitives/bignum.fst'
rm 'examples/primitives/buffer.fst'
rm 'examples/primitives/c/fstarlib.c'
rm 'examples/primitives/c/fstarlib.h'
rm 'examples/primitives/c/test_aes.c'
rm 'examples/primitives/c/test_bignum.c'
rm 'examples/primitives/c/test_chacha.c'
rm 'examples/primitives/c/test_curve.c'
rm 'examples/primitives/c/test_poly.c'
rm 'examples/primitives/chacha.fst'
rm 'examples/primitives/intlib.fst'
rm 'examples/primitives/ml/Buffer.ml'
rm 'examples/primitives/ml/SBuffer.ml'
rm 'examples/primitives/ml/SBytes.ml'
rm 'examples/primitives/ml/SInt_Cast.ml'
rm 'examples/primitives/ml/SInt_UInt32.ml'
rm 'examples/primitives/ml/SInt_UInt32.mli'
rm 'examples/primitives/ml/SInt_UInt63.ml'
rm 'examples/primitives/ml/SInt_UInt63.mli'
rm 'examples/primitives/ml/SInt_UInt64.ml'
rm 'examples/primitives/ml/SInt_UInt64.mli'
rm 'examples/primitives/ml/SInt_UInt8.ml'
rm 'examples/primitives/ml/SInt_UInt8.mli'
rm 'examples/primitives/ml/test_aes.ml'
rm 'examples/primitives/ml/test_chacha20.ml'
rm 'examples/primitives/ml/test_curve25519.ml'
rm 'examples/primitives/ml/test_poly1305.ml'
rm 'examples/primitives/parameters.fst'
rm 'examples/primitives/parameters1305.fst'
rm 'examples/primitives/poly.fst'
rm 'examples/primitives/sbuffer-experimental.fst'
rm 'examples/primitives/sbuffer.fst'
rm 'examples/primitives/sint.fst'
[hritcu@detained examples]$ git rm -r sgx (git)-[catalin_private]
rm 'examples/sgx/Ast.fst'
rm 'examples/sgx/FStar.SGX.fst'
rm 'examples/sgx/FStar.STX.fst'
rm 'examples/sgx/Interpreter.fst'
rm 'examples/sgx/Makefile'
rm 'examples/sgx/README'
rm 'examples/sgx/SGXState.fst'
rm 'examples/sgx/Test.fst'
rm 'examples/sgx/Util.fst'
rm 'examples/sgx/ml/main.ml'
rm 'examples/sgx/testsuite/Call.fst'
rm 'examples/sgx/verify/README'
rm 'examples/sgx/verify/VerAst.fst'
rm 'examples/sgx/verify/VerInterpreter.fst'
rm 'examples/sgx/verify/VerSGXState.fst'
rm 'examples/sgx/verify/VerTest.fst'
rm 'examples/sgx/verify/VerUtil.fst'
rm 'examples/sgx/verify/run.sh'
[hritcu@detained examples]$ git rm -r test (git)-[catalin_private]
rm 'examples/test/append_eq_singl.fst'
rm 'examples/test/ordmap.fst'
markulf
This branch is the last version of F* known to support the stratified language. https://github.com/FStarLang/FStar/tree/stratified_last This branch is frozen, i.e., don't push on this branch!
All the stratified-only examples that were once in the master tree have been removed (since commit 0fae595aa0aace5).
We should work to port all those examples forward to universes. To preserve the history of those examples, the recommended style is to work on a private fork of stratified_last, upgrade your example to make it work with master, and then merge those changes back in.
This issue will record all the examples that have been deleted and that we wish to restore.
[ ] examples/wysteria
[ ] examples/crypto
[ ] examples/metatheory (the main hurdle for updating these ~is~ was #580)
[ ] StlcCbvNamed
[ ] DbSubst
[ ] HereditarySubst
[ ] FOmega
[ ] MicroFStar
[ ] HoareWeakestPrecondition
[ ] StlcCbvDbPntSubstLists: This example is syntactically ok for universes, but it has 3 assertion failures. It remains in the master source tree (but has some problems #115)
[ ] examples/algorithms/counters.fst
[ ] examples/termination/ CPS.DoubleLambdaLifting.fst CPS.DoubleCC.fst <-- This one seems particularly problematic, as it may rely on Type:Type Eval.DBCC.fst
[ ]
examples/relationalSome of this has already been ported toexamples/rel[ ] examples/voting This relies on FStar.Relational.Relational
[ ] examples/paradoxes russell.fst berardi.fst
[ ]
examples/primitives(last version a21e94b9)[ ]
examples/sgx(last version a21e94b9) will need to bring back when it's ready contributors: Anitha Gollamudi, Aseem Rastogi[ ]
runtime/allocatorContributors: Abhishek Anand and Mike Hicks[ ] .old/to-be-ported (these examples are pre-stratified, dating from the fstar-0.7 series)
As of 2cc11626320, the uses of stratified code in the examples directory was: