Skip to content

Commit 7ce9d96

Browse files
authored
Merge branch 'master' into _fstar_dev_agent
2 parents 25bc52a + b4bc2ad commit 7ce9d96

37 files changed

Lines changed: 753 additions & 892 deletions

.github/workflows/release.yml

Lines changed: 21 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -7,13 +7,26 @@ on:
77
description: 'Dry run: just build, do not publish'
88
default: false
99
type: boolean
10+
target_sha:
11+
description: 'Commit SHA to release (default: HEAD of default branch)'
12+
default: ''
13+
type: string
14+
15+
concurrency:
16+
group: release
17+
cancel-in-progress: false
18+
19+
permissions:
20+
contents: write
1021

1122
env:
1223
DRY_RUN: ${{ github.event.inputs.dry_run || false }}
24+
# Use the provided SHA, or fall back to the SHA that triggered the workflow.
25+
TARGET_SHA: ${{ github.event.inputs.target_sha || github.sha }}
1326

1427
jobs:
15-
# Bump version number beforehand? I don't think the action can push
16-
# that to master (easily). Just remember to do so manually.
28+
# Bump version number beforehand, or use the weekly-release workflow
29+
# which automates the bump + release cycle.
1730

1831
# At least check for it, so we don't run this whole thing and fail
1932
# for an existing tag.
@@ -22,6 +35,7 @@ jobs:
2235
steps:
2336
- uses: actions/checkout@v6
2437
with:
38+
ref: ${{ env.TARGET_SHA }}
2539
submodules: true
2640
- if: env.DRY_RUN != 'true' # don't check on a dry run.
2741
run: |
@@ -35,6 +49,8 @@ jobs:
3549
build-all:
3650
needs: pre
3751
uses: ./.github/workflows/build-all.yml
52+
with:
53+
ref: ${{ github.event.inputs.target_sha || '' }}
3854

3955
publish:
4056
runs-on: ubuntu-latest
@@ -54,6 +70,7 @@ jobs:
5470

5571
- uses: actions/checkout@v6
5672
with:
73+
ref: ${{ env.TARGET_SHA }}
5774
submodules: true
5875
path: FStar
5976
- name: Rename packages to have version number
@@ -80,11 +97,11 @@ jobs:
8097
8198
TAG="v$V"
8299
# Create and push annotated tag to repo.
83-
git tag -a -m "F* version $V" "$TAG" "${{github.sha}}"
100+
git tag -a -m "F* version $V" "$TAG" "${{ env.TARGET_SHA }}"
84101
git push origin "$TAG"
85102
86103
# Create github release.
87-
gh release create --prerelease \
104+
gh release create --latest \
88105
--generate-notes \
89106
-t "F* v$V" \
90107
"$TAG" ../artifacts/*
Lines changed: 83 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,83 @@
1+
name: Update KaRaMeL submodule
2+
3+
# Automated weekly update of the karamel submodule.
4+
#
5+
# Creates a PR to fast-forward the submodule to upstream master
6+
# and lets CI gate the change. If auto-merge is enabled in repo
7+
# settings, the PR will be squash-merged automatically once CI
8+
# passes; otherwise it waits for a human to merge.
9+
10+
on:
11+
schedule:
12+
# Every Wednesday at noon UTC
13+
- cron: '0 12 * * 3'
14+
workflow_dispatch:
15+
16+
concurrency:
17+
group: update-karamel
18+
cancel-in-progress: false
19+
20+
permissions:
21+
contents: write
22+
pull-requests: write
23+
24+
jobs:
25+
update-karamel:
26+
runs-on: ubuntu-latest
27+
steps:
28+
- uses: actions/checkout@v6
29+
with:
30+
submodules: true
31+
32+
- name: Fast-forward karamel to upstream master
33+
id: update
34+
run: |
35+
cd karamel
36+
git fetch --unshallow # need full history for --ff-only
37+
git pull --ff-only origin master
38+
cd ..
39+
40+
git add karamel
41+
if git diff --cached --quiet; then
42+
echo "karamel submodule is already up to date."
43+
echo "skip=true" >> "$GITHUB_OUTPUT"
44+
else
45+
NEW_SHA=$(git -C karamel rev-parse --short HEAD)
46+
echo "new_sha=$NEW_SHA" >> "$GITHUB_OUTPUT"
47+
echo "skip=false" >> "$GITHUB_OUTPUT"
48+
fi
49+
50+
- name: Close stale auto-update PRs
51+
if: steps.update.outputs.skip != 'true'
52+
env:
53+
GH_TOKEN: ${{ github.token }}
54+
run: |
55+
gh pr list --state open --json number,headRefName \
56+
-q '.[] | select(.headRefName | startswith("auto/update-karamel-")) | .number' \
57+
| while read -r pr; do
58+
echo "Closing stale karamel update PR #$pr"
59+
gh pr close "$pr" --comment "Superseded by update to karamel ${{ steps.update.outputs.new_sha }}."
60+
done
61+
62+
- name: Create PR
63+
if: steps.update.outputs.skip != 'true'
64+
env:
65+
GH_TOKEN: ${{ github.token }}
66+
NEW_SHA: ${{ steps.update.outputs.new_sha }}
67+
run: |
68+
BRANCH="auto/update-karamel-$NEW_SHA"
69+
70+
git config user.name "Dzomo, the Everest Yak"
71+
git config user.email "24394600+dzomo@users.noreply.github.com"
72+
73+
git checkout -b "$BRANCH"
74+
git commit -m "Update karamel submodule to $NEW_SHA"
75+
git push origin "$BRANCH"
76+
77+
gh pr create \
78+
--title "Update karamel submodule to $NEW_SHA" \
79+
--body "Automated weekly fast-forward of the karamel submodule to upstream master ($NEW_SHA)." \
80+
--base master \
81+
--head "$BRANCH"
82+
83+
gh pr merge "$BRANCH" --auto --squash || echo "Auto-merge not available, PR requires manual merge."
Lines changed: 130 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,130 @@
1+
name: Weekly release
2+
3+
# Automated weekly version bump and release.
4+
#
5+
# Creates a PR to bump version.txt and fstar.opam to the current date,
6+
# enables auto-merge, waits for CI to pass and the PR to merge, then
7+
# dispatches the release workflow on the exact merge commit.
8+
#
9+
# Requirements:
10+
# - "Allow auto-merge" must be enabled in repo settings
11+
# - Branch protection must not require PR reviews (or the bot must
12+
# be able to satisfy them)
13+
14+
on:
15+
schedule:
16+
- cron: '0 12 * * 0' # Every Sunday at noon UTC
17+
workflow_dispatch:
18+
19+
concurrency:
20+
group: weekly-release
21+
cancel-in-progress: false
22+
23+
permissions:
24+
contents: write
25+
pull-requests: write
26+
actions: write
27+
28+
jobs:
29+
bump-and-release:
30+
runs-on: ubuntu-latest
31+
steps:
32+
- uses: actions/checkout@v6
33+
with:
34+
submodules: true
35+
fetch-depth: 0
36+
37+
- name: Compute new version
38+
id: version
39+
run: |
40+
NEW_VERSION=$(date -u +%Y.%m.%d)
41+
echo "new_version=$NEW_VERSION" >> "$GITHUB_OUTPUT"
42+
43+
git fetch --tags
44+
if git tag -l "v$NEW_VERSION" | grep -q .; then
45+
echo "::notice::Version v$NEW_VERSION already released, skipping"
46+
echo "skip=true" >> "$GITHUB_OUTPUT"
47+
else
48+
echo "skip=false" >> "$GITHUB_OUTPUT"
49+
fi
50+
51+
- name: Close stale auto-bump PRs
52+
if: steps.version.outputs.skip != 'true'
53+
env:
54+
GH_TOKEN: ${{ github.token }}
55+
run: |
56+
gh pr list --state open --json number,headRefName \
57+
-q '.[] | select(.headRefName | startswith("auto/bump-v")) | .number' \
58+
| while read -r pr; do
59+
echo "Closing stale auto-bump PR #$pr"
60+
gh pr close "$pr" --comment "Superseded by weekly bump to v${{ steps.version.outputs.new_version }}."
61+
done
62+
63+
- name: Bump version and create PR
64+
if: steps.version.outputs.skip != 'true'
65+
env:
66+
GH_TOKEN: ${{ secrets.DZOMO_GITHUB_TOKEN }}
67+
NEW_VERSION: ${{ steps.version.outputs.new_version }}
68+
run: |
69+
BRANCH="auto/bump-v$NEW_VERSION"
70+
71+
git config user.name "Dzomo, the Everest Yak"
72+
git config user.email "24394600+dzomo@users.noreply.github.com"
73+
74+
git checkout -b "$BRANCH"
75+
echo "$NEW_VERSION" > version.txt
76+
sed -i 's/^version: ".*"/version: "'"$NEW_VERSION"'~dev"/' fstar.opam
77+
git add version.txt fstar.opam
78+
git commit -m "Bump version to $NEW_VERSION"
79+
80+
# Push with PAT so that CI triggers on the PR
81+
git push "https://${{ secrets.DZOMO_GITHUB_TOKEN }}@github.com/${{ github.repository }}" "$BRANCH"
82+
83+
gh pr create \
84+
--title "Bump version to $NEW_VERSION" \
85+
--body "Automated weekly version bump for release v$NEW_VERSION." \
86+
--base master \
87+
--head "$BRANCH"
88+
89+
gh pr merge "$BRANCH" --auto --squash
90+
91+
- name: Wait for PR merge
92+
if: steps.version.outputs.skip != 'true'
93+
id: merged
94+
timeout-minutes: 180
95+
env:
96+
GH_TOKEN: ${{ github.token }}
97+
run: |
98+
BRANCH="auto/bump-v${{ steps.version.outputs.new_version }}"
99+
while true; do
100+
PR_JSON=$(gh pr view "$BRANCH" --json state,mergeCommit)
101+
STATE=$(echo "$PR_JSON" | jq -r '.state')
102+
if [[ "$STATE" == "MERGED" ]]; then
103+
MERGE_SHA=$(echo "$PR_JSON" | jq -r '.mergeCommit.oid')
104+
echo "PR merged at $MERGE_SHA"
105+
echo "merge_sha=$MERGE_SHA" >> "$GITHUB_OUTPUT"
106+
break
107+
elif [[ "$STATE" == "CLOSED" ]]; then
108+
echo "::error::PR was closed without merging"
109+
exit 1
110+
fi
111+
echo "PR state: $STATE, waiting..."
112+
sleep 60
113+
done
114+
115+
- name: Delete bump branch
116+
if: steps.version.outputs.skip != 'true' && steps.merged.outputs.merge_sha != ''
117+
env:
118+
GH_TOKEN: ${{ github.token }}
119+
run: |
120+
BRANCH="auto/bump-v${{ steps.version.outputs.new_version }}"
121+
git push origin --delete "$BRANCH" || true
122+
123+
- name: Trigger release
124+
if: steps.version.outputs.skip != 'true'
125+
env:
126+
GH_TOKEN: ${{ github.token }}
127+
run: |
128+
MERGE_SHA="${{ steps.merged.outputs.merge_sha }}"
129+
echo "Dispatching release.yml for commit $MERGE_SHA"
130+
gh workflow run release.yml -f target_sha="$MERGE_SHA"

examples/layeredeffects/SimpleHeap.fst

Lines changed: 0 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -3,7 +3,6 @@
33
*)
44
module SimpleHeap
55

6-
module S = FStar.Set
76
module F = FStar.FunctionalExtensionality
87

98
(** Internal cell type: stores a typed value *)

examples/layeredeffects/SimpleHeap.fsti

Lines changed: 0 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -7,7 +7,6 @@
77
module SimpleHeap
88

99
module S = FStar.Set
10-
module F = FStar.FunctionalExtensionality
1110

1211
(** The heap type *)
1312
val heap : Type u#1

fstar.opam

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -1,5 +1,5 @@
11
opam-version: "2.0"
2-
version: "2026.04.17~dev"
2+
version: "2026.05.03~dev"
33
maintainer: "guimartinez@microsoft.com"
44
authors: "Nik Swamy <nswamy@microsoft.com>,Jonathan Protzenko <protz@microsoft.com>,Tahina Ramananandro <taramana@microsoft.com>"
55
homepage: "http://fstar-lang.org"
@@ -13,7 +13,7 @@ depends: [
1313
"dune" {>= "3.8.0"}
1414
"memtrace" {>= "0.2.3"}
1515
"menhirLib"
16-
"menhir" {build & >= "20230415"}
16+
"menhir" {build & >= "20260112"}
1717
"mtime" {>= "2.1.0"}
1818
"pprint"
1919
"sedlex" {>= "3.5" }

pulse/share/pulse/examples/EqualOrDisjoint.fst

Lines changed: 0 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -1,8 +1,6 @@
11
module EqualOrDisjoint
22
#lang-pulse
33
open Pulse.Lib.Pervasives
4-
module R = Pulse.Lib.Reference
5-
module TR = Pulse.Lib.Trade
64
open Pulse.Lib.Trade
75
open Pulse.Lib.Forall.Util
86

pulse/share/pulse/examples/Quicksort.Base.fst

Lines changed: 0 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -19,7 +19,6 @@ module Quicksort.Base
1919

2020
open Pulse.Lib.Pervasives
2121
module A = Pulse.Lib.Array
22-
module R = Pulse.Lib.Reference
2322
module SZ = FStar.SizeT
2423
(* Base module with proof of correctness of Quicksort, partition, etc.
2524
#lang-pulse

pulse/share/pulse/examples/by-example/PulseByExample.fst

Lines changed: 0 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -49,7 +49,6 @@ fn five_alt ()
4949

5050
open Pulse.Lib.Reference
5151
open Pulse.Class.PtsTo
52-
module R = Pulse.Lib.Reference
5352

5453
(*
5554
Things to note:
@@ -114,7 +113,6 @@ fn test (r:ref int)
114113
}
115114

116115
open Pulse.Lib.Array
117-
module A = Pulse.Lib.Array
118116
module SZ = FStar.SizeT
119117
open Pulse.Lib.BoundedIntegers
120118

0 commit comments

Comments
 (0)