Code

Remove Steel from the F* code base#2889

Code

Merged

mtzguido merged 114 commits intomasterFStarLang/FStar:masterfrom taramana_no_steelFStarLang/FStar:taramana_no_steelCopy head branch name to clipboardMay 3, 2023

+30,291-222,600

Commits

Commits on Apr 12, 2023

• Karamel AST: add union and array types

  Show description for 4e0aabe
  tahina-pro

  committed
  4e0aabe

  Copy full SHA for 4e0aabe

• translate_type_without_decay; make C extraction modular

  Show description for a16763c
  tahina-pro

  committed
  a16763c

  Copy full SHA for a16763c

• use let _ =

  tahina-pro

  committed
  7ef4eab

  Copy full SHA for 7ef4eab

• snap

  tahina-pro

  committed
  38cef8c

  Copy full SHA for 38cef8c

• also make translate_let extensible

  tahina-pro

  committed
  57e1ab8

  Copy full SHA for 57e1ab8

• Revert "snap"

  Show description for b012c90
  tahina-pro

  committed
  b012c90

  Copy full SHA for b012c90

• snap

  tahina-pro

  committed
  17acd9e

  Copy full SHA for 17acd9e

• Revert "snap"

  Show description for 92b495c
  tahina-pro

  committed
  92b495c

  Copy full SHA for 92b495c

• split off the Steel extraction rules

  tahina-pro

  committed
  e0a4da8

  Copy full SHA for e0a4da8

• snap

  tahina-pro

  committed
  52183ff

  Copy full SHA for 52183ff

Commits on Apr 13, 2023

• remove Steel

  tahina-pro

  committed
  c83d43d

  Copy full SHA for c83d43d

• set some compatibility flag for FStar.NMST

  tahina-pro

  committed
  ef6288a

  Copy full SHA for ef6288a

• snap

  tahina-pro

  committed
  76a7d0a

  Copy full SHA for 76a7d0a

• (TEMP) use Karamel _taramana_no_steel

  tahina-pro

  committed
  1376c61

  Copy full SHA for 1376c61

• Steel bug report 2605 moved away

  tahina-pro

  committed
  1215aad

  Copy full SHA for 1215aad

• doc: disable ContextPollution

  tahina-pro

  committed
  8d066f6

  Copy full SHA for 8d066f6

• make FStar.Parser.Dep.core_modules a function

  Show description for 28ad84f
  tahina-pro

  committed
  28ad84f

  Copy full SHA for 28ad84f

• Revert "snap"

  Show description for 847b5b7
  tahina-pro

  committed
  847b5b7

  Copy full SHA for 847b5b7

• snap

  tahina-pro

  committed
  a8704c8

  Copy full SHA for a8704c8

• Revert "(TEMP) use Karamel _taramana_no_steel"

  Show description for bbbb9f0
  tahina-pro

  committed
  bbbb9f0

  Copy full SHA for bbbb9f0

• (TEMP) use Karamel taramana_no_steel

  tahina-pro

  committed
  afde4ee

  Copy full SHA for afde4ee

• Merge branch 'master' of github.com:FStarLang/FStar into taramana_no_steel

  tahina-pro

  committed
  df704e3

  Copy full SHA for df704e3

Commits on Apr 15, 2023

• remove Pulse

  tahina-pro

  committed
  55ada1b

  Copy full SHA for 55ada1b

• remove Steel

  tahina-pro

  committed
  cd951dc

  Copy full SHA for cd951dc

• Merge branch 'taramana_no_steel_merge_20230414' into taramana_no_steel

  tahina-pro

  committed
  dc98a9d

  Copy full SHA for dc98a9d

• advance F* version number to 2023.04.15

  tahina-pro

  committed
  d2376f9

  Copy full SHA for d2376f9

Commits on Apr 18, 2023

• Merge branch 'master' of github.com:FStarLang/FStar into taramana_no_steel

  tahina-pro

  committed
  c9cd885

  Copy full SHA for c9cd885

Commits on Apr 19, 2023

• two new reflection primitives: range_of_term and range_of_sigelt

  nikswamy

  committed
  1188f38

  Copy full SHA for 1188f38

Commits on Apr 20, 2023

• remove Pulse

  tahina-pro

  committed
  7cb2ee5

  Copy full SHA for 7cb2ee5

• Merge branch 'merge_20230419' into taramana_no_steel

  tahina-pro

  committed
  69b49e5

  Copy full SHA for 69b49e5

• more range utilities in reflection and tactics

  nikswamy

  committed
  55d5eb2

  Copy full SHA for 55d5eb2

• merging in guido_range

  nikswamy

  committed
  921dd41

  Copy full SHA for 921dd41

Commits on Apr 21, 2023

• bootstrap

  nikswamy

  committed
  44e3347

  Copy full SHA for 44e3347

• remove Steel and Pulse

  tahina-pro

  committed
  8efed96

  Copy full SHA for 8efed96

• partially revert a8704c8

  tahina-pro

  committed
  24ed334

  Copy full SHA for 24ed334

• Merge branch 'merge_20230420' into taramana_no_steel

  tahina-pro

  committed
  2c866d8

  Copy full SHA for 2c866d8

• snap

  tahina-pro

  committed
  ff6cdf4

  Copy full SHA for ff6cdf4

• merging master in

  aseemr

  committed
  d36f875

  Copy full SHA for d36f875

• Merge branch 'taramana_no_steel' of github:FStarLang/FStar into guido_range

  mtzguido

  committed
  b419530

  Copy full SHA for b419530

• Merge pull request #2884 from FStarLang/guido_range

  Show description for 20039e9
  nikswamy

  authored
  20039e9

  Copy full SHA for 20039e9

Commits on Apr 24, 2023

• Merge branch 'master' into taramana_no_steel

  aseemr

  committed
  3b18d53

  Copy full SHA for 3b18d53

• basic: split GenSym into own module

  mtzguido

  committed
  f489d54

  Copy full SHA for f489d54

• nits on Makefile

  mtzguido

  committed
  f5813e6

  Copy full SHA for f5813e6

• run_benchmark: update

  mtzguido

  committed
  64c256b

  Copy full SHA for 64c256b

• syntax: visit: nits

  mtzguido

  committed
  7688624

  Copy full SHA for 7688624

• tc: rel: small fix, freshen+open required

  mtzguido

  committed
  c7a1060

  Copy full SHA for c7a1060

• snap

  mtzguido

  committed
  e325c72

  Copy full SHA for e325c72

• examples: removing some old, time-consuming examples from CI

  mtzguido

  committed
  36e8bdf

  Copy full SHA for 36e8bdf

• ulib: simplify extraction makefiles, add depgraph rule

  mtzguido

  committed
  daffd96

  Copy full SHA for daffd96

• Makefile.arraystruct: remove stale Makefile

  mtzguido

  committed
  ef724cf

  Copy full SHA for ef724cf

• gen_mllib: remove now unneeded script

  mtzguido

  committed
  ffdfc27

  Copy full SHA for ffdfc27

• ulib: ml: Makefile nit

  mtzguido

  committed
  961ce10

  Copy full SHA for 961ce10

• snap

  mtzguido

  committed
  9d98ab0

  Copy full SHA for 9d98ab0

Commits on Apr 25, 2023

• merging in taramana_no_steel

  nikswamy

  committed
  38e77ee

  Copy full SHA for 38e77ee

• Merge pull request #2887 from FStarLang/nik_range_of_term

  Show description for b2fdb81
  nikswamy

  authored
  b2fdb81

  Copy full SHA for b2fdb81

• [CI] regenerate hints + ocaml snapshot

  

  Dzomo, the Everest Yak

  committed
  912920f

  Copy full SHA for 912920f

• [CI] bump version number to 2023.04.25~dev

  

  Dzomo, the Everest Yak

  committed
  d202003

  Copy full SHA for d202003

• Merge pull request #2888 from FStarLang/_BuildHints-_release

  Show description for 4e8f5d1
  tahina-pro

  authored
  4e8f5d1

  Copy full SHA for 4e8f5d1

• Revert "[CI] bump version number to 2023.04.25~dev"

  Show description for 3baeb5d
  tahina-pro

  committed
  3baeb5d

  Copy full SHA for 3baeb5d

• remove Steel and Pulse hints

  tahina-pro

  committed
  6c66ddc

  Copy full SHA for 6c66ddc

• revert conflicting hint

  tahina-pro

  committed
  757853e

  Copy full SHA for 757853e

• Merge branch '_release_merge_20230425' into taramana_no_steel

  tahina-pro

  committed
  30776e2

  Copy full SHA for 30776e2

• bump version number to 2023.04.26~dev

  tahina-pro

  committed
  5ee8f31

  Copy full SHA for 5ee8f31

• (TEMP) CI: ignore branch taramana_no_steel

  tahina-pro

  committed
  b0bc6c8

  Copy full SHA for b0bc6c8

Commits on Apr 26, 2023

• Merge branch 'guido_range' of github:FStarLang/FStar

  mtzguido

  committed
  fd4a8e1

  Copy full SHA for fd4a8e1

Commits on Apr 27, 2023

• tosyntax: propagate sigelt attributes to each letbinding

  Show description for 0828cf5
  mtzguido

  committed
  0828cf5

  Copy full SHA for 0828cf5

• tc: keep attributes from original letbindings even when there is a val

  Show description for f9b9833
  mtzguido

  committed
  f9b9833

  Copy full SHA for f9b9833

• introduce an admit_termination attribute

  Show description for e646106
  mtzguido

  committed
  e646106

  Copy full SHA for e646106

• tests: add a test for @@admit_termination

  mtzguido

  committed
  6267638

  Copy full SHA for 6267638

• tc: change the effect annotation for Sig_let

  mtzguido

  committed
  ab74f5c

  Copy full SHA for ab74f5c

• snap

  mtzguido

  committed
  364cbcd

  Copy full SHA for 364cbcd

• update test

  mtzguido

  committed
  6c6536c

  Copy full SHA for 6c6536c

• ulib: starting a userland verified term_eq

  mtzguido

  committed
  53197a7

  Copy full SHA for 53197a7

• ulib: termeq: more cases

  mtzguido

  committed
  ef72680

  Copy full SHA for ef72680

• Merge pull request #2896 from FStarLang/guido_misc

  Show description for f89ee53
  mtzguido

  authored
  f89ee53

  Copy full SHA for f89ee53

• Revert "(TEMP) CI: ignore branch taramana_no_steel"

  Show description for e509dad
  tahina-pro

  committed
  e509dad

  Copy full SHA for e509dad

• snap

  mtzguido

  committed
  c375e11

  Copy full SHA for c375e11

• examples: dsl: update

  mtzguido

  committed
  e38c34e

  Copy full SHA for e38c34e

• reflection: no BV sorts

  mtzguido

  committed
  d53e606

  Copy full SHA for d53e606

• snap

  mtzguido

  committed
  f4a26d0

  Copy full SHA for f4a26d0

• tactics: make fresh_bv not take a type arg

  mtzguido

  committed
  ab9c201

  Copy full SHA for ab9c201

Commits on Apr 28, 2023

• tests: tactics: update for no bv sort

  mtzguido

  committed
  a439964

  Copy full SHA for a439964

• WIP disable param

  mtzguido

  committed
  6d8688e

  Copy full SHA for 6d8688e

• nits

  aseemr

  committed
  07b677a

  Copy full SHA for 07b677a

• proof for open_with_gt_ln

  aseemr

  committed
  2f25008

  Copy full SHA for 2f25008

• proof for equiv_abs_close

  aseemr

  committed
  d8aff98

  Copy full SHA for d8aff98

• Merge branch 'taramana_no_steel' into _aseem_taramana_no_steel

  aseemr

  committed
  9957c4f

  Copy full SHA for 9957c4f

• snap

  aseemr

  committed
  01093d5

  Copy full SHA for 01093d5

• fix examples

  mtzguido

  committed
  fd1d643

  Copy full SHA for fd1d643

• Merge branch 'taramana_no_steel' of github:FStarLang/FStar into dsl

  mtzguido

  committed
  68bd6f2

  Copy full SHA for 68bd6f2

Commits on May 1, 2023

• syntax: print: a fix for vale

  mtzguido

  committed
  94d5280

  Copy full SHA for 94d5280

• snap

  mtzguido

  committed
  eded8f3

  Copy full SHA for eded8f3

• syntax: print: a fix for vale

  mtzguido

  committed
  d9bd7e4

  Copy full SHA for d9bd7e4

• snap

  mtzguido

  committed
  394df67

  Copy full SHA for 394df67

Commits on May 2, 2023

• wip, adding ghost effect to reflection typing

  aseemr

  committed
  9d18913

  Copy full SHA for 9d18913

• fixes in FStar.Reflection.Typing.fst

  aseemr

  committed
  4f273df

  Copy full SHA for 4f273df

• effect label type on the src side

  aseemr

  committed
  213d528

  Copy full SHA for 213d528

• snap

  aseemr

  committed
  549eac3

  Copy full SHA for 549eac3

• embeddings for effect_label

  aseemr

  committed
  3208686

  Copy full SHA for 3208686

• snap

  aseemr

  committed
  c199b0d

  Copy full SHA for c199b0d

• fixes to meta APIs to take effect label

  aseemr

  committed
  8dfd318

  Copy full SHA for 8dfd318

• snap

  aseemr

  committed
  db127ec

  Copy full SHA for db127ec

• Merge branch 'taramana_no_steel' of github.com:FStarLang/FStar into guido_no_steel

  mtzguido

  committed
  37130b6

  Copy full SHA for 37130b6

• Merge branch 'master' of github.com:FStarLang/FStar into guido_no_steel

  mtzguido

  committed
  f9dd78f

  Copy full SHA for f9dd78f

Commits on May 3, 2023

• abbreviations for tot and ghost typing

  aseemr

  committed
  d3a96af

  Copy full SHA for d3a96af

• snap

  aseemr

  committed
  404adea

  Copy full SHA for 404adea

• some nits to reflection typing

  aseemr

  committed
  e83bfb1

  Copy full SHA for e83bfb1

• changing effect_label to tot_or_gtot

  aseemr

  committed
  36a6c0f

  Copy full SHA for 36a6c0f

• snap

  aseemr

  committed
  4734327

  Copy full SHA for 4734327

• snap

  aseemr

  committed
  312a052

  Copy full SHA for 312a052

• Merge branch 'master' into taramana_no_steel

  aseemr

  committed
  e75e3ee

  Copy full SHA for e75e3ee

• Merge branch 'taramana_no_steel' into aseem_ghost_reflection

  aseemr

  committed
  e21853d

  Copy full SHA for e21853d

• fixing other dsls

  aseemr

  committed
  bde73ec

  Copy full SHA for bde73ec

• Revert "(TEMP) use Karamel taramana_no_steel"

  Show description for 4ab5019
  mtzguido

  committed
  4ab5019

  Copy full SHA for 4ab5019