Skip to content

Commit 2abb0d3

Browse files
nikswamynikswamy
committed
Merge remote-tracking branch 'origin/fstar2' into fstar2_remove_ulevel_nat_axiom
2 parents d7b29dc + 1cb0aca commit 2abb0d3

File tree

208 files changed

+709
-20324
lines changed

Some content is hidden

Large Commits have some content hidden by default. Use the searchbox below for content that may be hidden.

208 files changed

+709
-20324
lines changed

‎.github/workflows/bench.yml‎

Lines changed: 2 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -90,12 +90,14 @@ jobs:
9090
with:
9191
ref: ${{ steps.pr.outputs.base_sha }}
9292
path: fstar-base
93+
submodules: true
9394

9495
- name: Checkout head
9596
uses: actions/checkout@v6
9697
with:
9798
ref: ${{ steps.pr.outputs.head_sha }}
9899
path: fstar-head
100+
submodules: true
99101

100102
# Run full CI (build + tests) sequentially with resource monitoring.
101103
# Building the compiler is included since F* is bootstrapped.

‎.github/workflows/build-all.yml‎

Lines changed: 10 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -2,6 +2,10 @@ name: Build F* binaries (all archs)
22

33
on:
44
workflow_call:
5+
inputs:
6+
ref:
7+
type: string
8+
default: ''
59
workflow_dispatch:
610

711
jobs:
@@ -11,9 +15,15 @@ jobs:
1115

1216
linux:
1317
uses: ./.github/workflows/build-linux.yml
18+
with:
19+
ref: ${{ inputs.ref || '' }}
1420

1521
macos:
1622
uses: ./.github/workflows/build-macos.yml
23+
with:
24+
ref: ${{ inputs.ref || '' }}
1725

1826
windows:
1927
uses: ./.github/workflows/build-windows.yml
28+
with:
29+
ref: ${{ inputs.ref || '' }}

‎.github/workflows/build-ci.yml‎

Lines changed: 7 additions & 7 deletions
Original file line numberDiff line numberDiff line change
@@ -31,8 +31,9 @@ jobs:
3131
- uses: actions/checkout@master
3232
with:
3333
path: FStar
34+
submodules: true
3435

35-
- name: Produce all artifacts
36+
- name: Produce binary package + source package
3637
run: |
3738
# Note: we don't package Z3 for the CI artifact as the images
3839
# already have the relevant Z3.
@@ -51,13 +52,12 @@ jobs:
5152
name: fstar-src.tar.gz
5253
retention-days: 3
5354

54-
# Upload full repo too, for stage3 check and Pulse. Note: we
55-
# explicitly run 'make setlink-2' at this point to generate the out/
56-
# directory, as the previous targets do not. Also, remove the
57-
# previous archives so they don't blow up the size of this
58-
# artifact.
55+
# Upload full repo too, for boot diff check. Note: we explicitly run 'make
56+
# stage3' at this point to generate the out/ directory, as the previous
57+
# targets do not. Also, remove the previous archives so they don't blow up
58+
# the size of this artifact.
5959
- run: rm -f FStar/fstar*.tar.gz
60-
- run: make setlink-2
60+
- run: make stage3
6161
working-directory: FStar
6262

6363
- uses: mtzguido/gci-upload@master

‎.github/workflows/build-linux.yml‎

Lines changed: 15 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -5,6 +5,10 @@ name: Build F* (Linux)
55

66
on:
77
workflow_call:
8+
inputs:
9+
ref:
10+
type: string
11+
default: ''
812
workflow_dispatch:
913

1014
defaults:
@@ -18,6 +22,9 @@ jobs:
1822
# all more recent versions.
1923
steps:
2024
- uses: actions/checkout@master
25+
with:
26+
ref: ${{ inputs.ref || '' }}
27+
submodules: true
2128

2229
- uses: ocaml/setup-ocaml@v3
2330
with:
@@ -34,7 +41,12 @@ jobs:
3441
# Setting FSTAR_VERSION for nightly and release builds. If unset,
3542
# we use $(version.txt)~dev. Setting it avoids the ~dev.
3643
if [[ "${{github.workflow_ref}}" =~ "nightly.yml" ]]; then
37-
echo FSTAR_VERSION="nightly-$(date -I)" >> $GITHUB_ENV
44+
REF="${{ inputs.ref }}"
45+
if [[ -n "$REF" && "$REF" != "master" ]]; then
46+
echo FSTAR_VERSION="nightly-${REF}-$(date -I)" >> $GITHUB_ENV
47+
else
48+
echo FSTAR_VERSION="nightly-$(date -I)" >> $GITHUB_ENV
49+
fi
3850
elif [[ "${{github.workflow_ref}}" =~ "release.yml" ]]; then
3951
echo FSTAR_VERSION="$(cat version.txt)" >> $GITHUB_ENV
4052
echo FSTAR_RELEASE=1 >> $GITHUB_ENV
@@ -87,3 +99,5 @@ jobs:
8799
./fstar/bin/fstar.exe fstar/lib/fstar/ulib/Prims.fst -f
88100
echo -e "module A\nopen FStar.Mul\nlet _ = assert (forall x. 1 + x*x > 0)" > A.fst
89101
./fstar/bin/fstar.exe A.fst
102+
echo -e "module B\n#lang-pulse\nopen Pulse\nfn test (x:int) returns int { (x+1); }" > B.fst
103+
./fstar/bin/fstar.exe --admit_smt_queries true B.fst

‎.github/workflows/build-macos.yml‎

Lines changed: 15 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -3,12 +3,19 @@ name: Build F* (macos)
33
on:
44
workflow_dispatch:
55
workflow_call:
6+
inputs:
7+
ref:
8+
type: string
9+
default: ''
610

711
jobs:
812
build:
913
runs-on: macos-14
1014
steps:
1115
- uses: actions/checkout@master
16+
with:
17+
ref: ${{ inputs.ref || '' }}
18+
submodules: true
1219

1320
- uses: ocaml/setup-ocaml@v3
1421
with:
@@ -26,7 +33,12 @@ jobs:
2633
# Setting FSTAR_VERSION for nightly and release builds. If unset,
2734
# we use $(version.txt)~dev. Setting it avoids the ~dev.
2835
if [[ "${{github.workflow_ref}}" =~ "nightly.yml" ]]; then
29-
echo FSTAR_VERSION="nightly-$(date -I)" >> $GITHUB_ENV
36+
REF="${{ inputs.ref }}"
37+
if [[ -n "$REF" && "$REF" != "master" ]]; then
38+
echo FSTAR_VERSION="nightly-${REF}-$(date -I)" >> $GITHUB_ENV
39+
else
40+
echo FSTAR_VERSION="nightly-$(date -I)" >> $GITHUB_ENV
41+
fi
3042
elif [[ "${{github.workflow_ref}}" =~ "release.yml" ]]; then
3143
echo FSTAR_VERSION="$(cat version.txt)" >> $GITHUB_ENV
3244
echo FSTAR_RELEASE=1 >> $GITHUB_ENV
@@ -73,3 +85,5 @@ jobs:
7385
./fstar/bin/fstar.exe --admit_smt_queries true fstar/lib/fstar/ulib/Prims.fst -f
7486
echo -e "module A\nopen FStar.Mul\nlet _ = assert (forall x. 1 + x*x > 0)" > A.fst
7587
./fstar/bin/fstar.exe --admit_smt_queries true A.fst
88+
echo -e "module B\n#lang-pulse\nopen Pulse\nfn test (x:int) returns int { (x+1); }" > B.fst
89+
./fstar/bin/fstar.exe --admit_smt_queries true B.fst

‎.github/workflows/build-opam.yml‎

Lines changed: 4 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -22,6 +22,8 @@ jobs:
2222
runs-on: ubuntu-latest
2323
steps:
2424
- uses: actions/checkout@master
25+
with:
26+
submodules: true
2527

2628
- uses: ocaml/setup-ocaml@v3
2729
with:
@@ -37,3 +39,5 @@ jobs:
3739
run: |
3840
echo -e "module A\nopen FStar.Mul\nlet _ = assert (forall x. 1 + x*x > 0)" > A.fst
3941
eval $(opam env) && fstar.exe A.fst
42+
echo -e "module B\n#lang-pulse\nopen Pulse\nfn test (x:int) returns int { (x+1); }" > B.fst
43+
eval $(opam env) && fstar.exe B.fst

‎.github/workflows/build-src.yml‎

Lines changed: 13 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -2,6 +2,10 @@ name: Build F* (src)
22

33
on:
44
workflow_call:
5+
inputs:
6+
ref:
7+
type: string
8+
default: ''
59
workflow_dispatch:
610

711
defaults:
@@ -16,6 +20,9 @@ jobs:
1620
steps:
1721
- uses: actions/checkout@master
1822
id: checkout
23+
with:
24+
ref: ${{ inputs.ref || '' }}
25+
submodules: true
1926

2027
- name: Check cache
2128
id: check-cache
@@ -39,7 +46,12 @@ jobs:
3946
# Setting FSTAR_VERSION for nightly and release builds. If unset,
4047
# we use $(version.txt)~dev. Setting it avoids the ~dev.
4148
if [[ "${{github.workflow_ref}}" =~ "nightly.yml" ]]; then
42-
echo FSTAR_VERSION="nightly-$(date -I)" >> $GITHUB_ENV
49+
REF="${{ inputs.ref }}"
50+
if [[ -n "$REF" && "$REF" != "master" ]]; then
51+
echo FSTAR_VERSION="nightly-${REF}-$(date -I)" >> $GITHUB_ENV
52+
else
53+
echo FSTAR_VERSION="nightly-$(date -I)" >> $GITHUB_ENV
54+
fi
4355
elif [[ "${{github.workflow_ref}}" =~ "release.yml" ]]; then
4456
echo FSTAR_VERSION="$(cat version.txt)" >> $GITHUB_ENV
4557
echo FSTAR_RELEASE=1 >> $GITHUB_ENV

‎.github/workflows/build-windows.yml‎

Lines changed: 14 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -12,6 +12,10 @@ name: Build F* (Windows)
1212

1313
on:
1414
workflow_call:
15+
inputs:
16+
ref:
17+
type: string
18+
default: ''
1519
workflow_dispatch:
1620

1721
defaults:
@@ -23,6 +27,8 @@ jobs:
2327
# We begin from a source package (built in Linux)
2428
build-src:
2529
uses: ./.github/workflows/build-src.yml
30+
with:
31+
ref: ${{ inputs.ref || '' }}
2632

2733
build:
2834
needs: build-src
@@ -68,7 +74,12 @@ jobs:
6874
# Setting FSTAR_VERSION for nightly and release builds. If unset,
6975
# we use $(version.txt)~dev. Setting it avoids the ~dev.
7076
if [[ "${{github.workflow_ref}}" =~ "nightly.yml" ]]; then
71-
echo FSTAR_VERSION="nightly-$(date -I)" >> $GITHUB_ENV
77+
REF="${{ inputs.ref }}"
78+
if [[ -n "$REF" && "$REF" != "master" ]]; then
79+
echo FSTAR_VERSION="nightly-${REF}-$(date -I)" >> $GITHUB_ENV
80+
else
81+
echo FSTAR_VERSION="nightly-$(date -I)" >> $GITHUB_ENV
82+
fi
7283
elif [[ "${{github.workflow_ref}}" =~ "release.yml" ]]; then
7384
echo FSTAR_VERSION="$(cat FStar/version.txt)" >> $GITHUB_ENV
7485
fi
@@ -172,3 +183,5 @@ jobs:
172183
$PSDefaultParameterValues['Out-File:Encoding'] = 'utf8' # Make sure we write UTF-8 files
173184
echo "module A`nopen FStar.Mul`nlet _ = assert (forall x. 1 + x*x > 0)" > A.fst
174185
.\fstar\bin\fstar.exe --already_cached *,-A A.fst
186+
echo "module B`n#lang-pulse`nopen Pulse`nfn test (x:int) returns int { (x+1); }" > B.fst
187+
.\fstar\bin\fstar.exe B.fst

‎.github/workflows/nightly-schedule.yml‎

Lines changed: 22 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,22 @@
1+
name: Nightly schedule
2+
3+
# This workflow dispatches nightly.yml for each branch that needs a
4+
# nightly build. To add a new branch, just add it to the matrix below.
5+
6+
on:
7+
schedule:
8+
- cron: '0 0 * * *'
9+
10+
permissions:
11+
actions: write
12+
13+
jobs:
14+
dispatch:
15+
runs-on: ubuntu-latest
16+
strategy:
17+
matrix:
18+
branch: [master, fstar2]
19+
steps:
20+
- run: gh workflow run nightly.yml -f branch=${{ matrix.branch }}
21+
env:
22+
GH_TOKEN: ${{ github.token }}

‎.github/workflows/nightly.yml‎

Lines changed: 24 additions & 5 deletions
Original file line numberDiff line numberDiff line change
@@ -8,23 +8,33 @@ name: F* nightly build
88
#
99
# The default GITHUB_TOKEN only allows access to the current repo, so it's
1010
# not useful.
11+
#
12+
# Nightly builds are scheduled by nightly-schedule.yml, which dispatches
13+
# this workflow for each branch. You can also trigger it manually.
1114

1215
on:
13-
schedule:
14-
- cron: '0 0 * * *'
1516
workflow_dispatch:
17+
inputs:
18+
branch:
19+
description: 'Branch to build'
20+
type: string
21+
default: 'master'
1622

1723
jobs:
1824
build-all:
1925
uses: ./.github/workflows/build-all.yml
26+
with:
27+
ref: ${{ inputs.branch }}
2028

2129
publish:
2230
runs-on: ubuntu-latest
2331
needs: build-all
2432
steps:
2533
- uses: actions/checkout@master
2634
with:
35+
ref: ${{ inputs.branch }}
2736
fetch-depth: 0 # full clone, so we can push objects
37+
submodules: true
2838

2939
- name: Set up git and some variables
3040
run: |
@@ -33,10 +43,19 @@ jobs:
3343
3444
# We push nightly builds to a different repo (same org)
3545
REPO="${{github.repository}}-nightly"
36-
TAG=nightly-$(date -I)
46+
47+
BRANCH="${{ inputs.branch }}"
48+
if [[ "$BRANCH" == "master" ]]; then
49+
TAG=nightly-$(date -I)
50+
else
51+
TAG=nightly-${BRANCH}-$(date -I)
52+
fi
53+
54+
SHA=$(git rev-parse HEAD)
3755
3856
echo "REPO=$REPO" >>$GITHUB_ENV
3957
echo "TAG=$TAG" >>$GITHUB_ENV
58+
echo "SHA=$SHA" >>$GITHUB_ENV
4059
4160
- uses: actions/download-artifact@v8
4261
with:
@@ -61,7 +80,7 @@ jobs:
6180
6281
- name: Create tag
6382
run: |
64-
git tag $TAG ${{github.sha}}
83+
git tag $TAG $SHA
6584
6685
- name: Push tag to nightly repo
6786
run: |
@@ -74,7 +93,7 @@ jobs:
7493
run: |
7594
gh release create -R "$REPO" \
7695
--generate-notes \
77-
--target ${{ github.sha }} \
96+
--target $SHA \
7897
$TAG artifacts/*
7998
echo "Done!"
8099

0 commit comments

Comments
 (0)