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

Staged build, new CI, new packaging #3637

Draft
wants to merge 33 commits into
base: master
Choose a base branch
from
Draft
Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
33 commits
Select commit Hold shift + click to select a range
4d51e0e
Remove ocaml/, move manual files into src/ml and ulib/ml
mtzguido Oct 14, 2024
791b6e8
Coallesce nix files into .nix
mtzguido Oct 14, 2024
004b37a
version.txt: v0.9.9 (unclear)
mtzguido Oct 14, 2024
704325e
src: removing old makefiles
mtzguido Oct 14, 2024
eebdd88
Remove bin/, move scripts to .scripts
mtzguido Oct 14, 2024
9c387bc
Plugins: compiling against fstar_plugin_lib and autoloading it
mtzguido Oct 14, 2024
648bc10
guts, pluginnolib
mtzguido Oct 14, 2024
cc89ef4
New staged build system (without stage0)
mtzguido Oct 14, 2024
3a2f30d
stage0, from master
mtzguido Oct 16, 2024
ffcc04a
VS code configs
mtzguido Oct 18, 2024
c5dc246
Update tests for new build
mtzguido Oct 23, 2024
ad94dfc
FStar.Buffer.fst: flaky proof
mtzguido Dec 20, 2024
052bc12
Restore F* library build
mtzguido Dec 20, 2024
e918872
New CI
mtzguido Oct 14, 2024
d7d600b
CI: No self-hosted, again
mtzguido Dec 21, 2024
b4963d0
tests: nits
mtzguido Dec 21, 2024
8ce739f
stage.mk: do not blast directory before installing
mtzguido Dec 21, 2024
599f5d2
Update test rules
mtzguido Dec 21, 2024
93002c9
Preserve timestamps when installing lib files
mtzguido Dec 26, 2024
edc5f5f
Makefile: Update package rules
mtzguido Dec 27, 2024
700e891
Makefile: Fix typo in help
mtzguido Dec 27, 2024
cc08ab2
lib.mk: use Z3 4.13.3
mtzguido Dec 28, 2024
17c3425
lib.mk: enable context pruning
mtzguido Dec 28, 2024
c5feda6
ci: simplify nightly job (missing: uploading binaries)
mtzguido Dec 30, 2024
07e9021
ci: use sudo for deletion
mtzguido Dec 30, 2024
bb0e24e
lib.mk: do not use automatic dep analysis, give explicit roots
mtzguido Dec 31, 2024
b6b4edd
ulib: remove reclaimable/ directory
mtzguido Dec 31, 2024
1153c85
ulib: remove stray hint files, they are now in .hints
mtzguido Dec 31, 2024
dccda2a
src_package_mk: nits
mtzguido Dec 31, 2024
eeef067
ci.yml: do not force rebuild when testing
mtzguido Dec 31, 2024
4d7b151
stageN: nits in dune files
mtzguido Dec 31, 2024
7adf5d4
Makefile: tweak 'ci' rule
mtzguido Jan 1, 2025
8aaa60c
stage.mk: use dune --release instead of custom flags
mtzguido Jan 1, 2025
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
  •  
  •  
  •  
63 changes: 0 additions & 63 deletions .common.mk

This file was deleted.

58 changes: 58 additions & 0 deletions .docker/dev-base.Dockerfile
Original file line number Diff line number Diff line change
@@ -0,0 +1,58 @@
FROM ubuntu:24.04

RUN apt-get update

RUN apt-get install -y --no-install-recommends \
git \
sudo \
python3 \
python-is-python3 \
opam \
rustc \
curl \
ca-certificates \
rsync \
wget \
&& apt-get clean -y

# Install the relevant Z3 versions.
COPY ./bin/get_fstar_z3.sh /usr/local/bin
RUN get_fstar_z3.sh /usr/local/bin

RUN useradd -ms /bin/bash user
RUN echo 'user ALL=NOPASSWD: ALL' >> /etc/sudoers
USER user
WORKDIR /home/user

# Install OCaml
ARG OCAML_VERSION=4.14.2
RUN opam init --compiler=$OCAML_VERSION --disable-sandboxing
RUN opam env --set-switch | tee --append $HOME/.profile $HOME/.bashrc $HOME/.bash_profile
RUN opam option depext-run-installs=true
ENV OPAMYES=1

# F* dependencies. This is the only place where we read a file from
# the F* repo.
ADD fstar.opam ./fstar.opam
RUN opam install -j$(nproc) --confirm-level=unsafe-yes --deps-only ./fstar.opam && opam clean

# Some karamel dependencies too. hex for everparse
RUN opam install -j$(nproc) --confirm-level=unsafe-yes fix fileutils visitors camlp4 wasm ulex uucp ctypes ctypes-foreign hex && opam clean

RUN sudo apt install time

# Sigh, install dotnet. The setup-dotnet action does not
# work on a container apparently.
ENV DOTNET_ROOT /dotnet
RUN wget -nv https://download.visualstudio.microsoft.com/download/pr/cd0d0a4d-2a6a-4d0d-b42e-dfd3b880e222/008a93f83aba6d1acf75ded3d2cfba24/dotnet-sdk-6.0.400-linux-x64.tar.gz && \
sudo mkdir -p $DOTNET_ROOT && \
sudo tar xf dotnet-sdk-6.0.400-linux-x64.tar.gz -C $DOTNET_ROOT && \
rm -f dotnet-sdk*.tar.gz
RUN sudo ln -s $DOTNET_ROOT/dotnet /usr/local/bin/dotnet

RUN rm fstar.opam # move up

# install rust (move up and remove rustv)
RUN curl --proto '=https' --tlsv1.2 -sSf https://sh.rustup.rs | sh -s -- -y
RUN sudo apt-get update && sudo apt-get install --yes --no-install-recommends llvm-dev libclang-dev clang libgmp-dev pkg-config
RUN . "$HOME/.cargo/env" && rustup component add rustfmt && cargo install bindgen-cli
6 changes: 0 additions & 6 deletions .github/env.sh

This file was deleted.

18 changes: 0 additions & 18 deletions .github/setup-macos.sh

This file was deleted.

76 changes: 76 additions & 0 deletions .github/workflows/build.yml
Original file line number Diff line number Diff line change
@@ -0,0 +1,76 @@
name: Build F*

on:
workflow_call:
workflow_dispatch:

defaults:
run:
shell: bash

jobs:
build:
# Build an F* binary package: a fully-bootstrapped stage 2 compiler,
# with its plugins, a fully checked library (i.e. with .checked)
# files and compiled versions of fstar_lib and fstar_plugin_lib.
# Also, we build a full stage 1 compiler and its libraries, and
# make all possible artifacts.
# runs-on: [self-hosted, linux, X64] # self-hosted so we use fast runners
runs-on: ubuntu-latest
container: mtzguido/dev-base
steps:
- name: Cleanup
run: sudo find . -delete
- run: echo "HOME=/home/user" >> $GITHUB_ENV
- uses: mtzguido/set-opam-env@master

- name: Checkout
uses: actions/checkout@master
with:
path: FStar

- name: Produce all artifacts
run: make -skj$(nproc) all-packages FSTAR_VERSION=ci ADMIT=1
working-directory: FStar

# Upload the archives.
- uses: actions/upload-artifact@v4
with:
path: FStar/fstar-ci.tar.gz
name: fstar-ci.tar.gz
retention-days: 3
- uses: actions/upload-artifact@v4
with:
path: FStar/fstar-ci-stage1.tar.gz
name: fstar-ci-stage1.tar.gz
retention-days: 3
- uses: actions/upload-artifact@v4
with:
path: FStar/fstar-ci-src.tar.gz
name: fstar-ci-src.tar.gz
retention-days: 3
- uses: actions/upload-artifact@v4
with:
path: FStar/fstar-ci-stage1-src.tar.gz
name: fstar-ci-stage1-src.tar.gz
retention-days: 3

# Upload full repo too, for stage3 check and Pulse. Note: we
# explicitly run 'make 2' at this point to generate the out/
# directory, as the previous targets do not. Also, remove the
# previous archives so they don't blow up the size of this
# artifact.
- run: rm -f FStar/fstar-ci*.tar.gz
- run: make 2
working-directory: FStar

- uses: mtzguido/gci-upload@master
with:
name: fstar-repo
path: FStar
extra: --exclude=FStar/stage*/dune/_build
hometag: FSTAR

# FIXME: Ideally, we could upload the artifacts as soon as each of
# them is created, and start the subsequent jobs at that instant too.
# Is that even doable...?
Loading
Loading