Use F* binary release.

Author: gebner

.devcontainer/Containerfile

@@ -2,7 +2,7 @@ FROM mcr.microsoft.com/devcontainers/base:ubuntu
 
 RUN apt-get update && \
     apt-get install -y --no-install-recommends \
-        opam pkg-config libgmp-dev tmux ripgrep tig gdb \
+        pkg-config libgmp-dev tmux ripgrep tig gdb \
         clang clang-format ccls zstd rustup \
         lsb-release wget software-properties-common gnupg && \
     apt-get clean
@@ -16,20 +16,10 @@ RUN wget https://apt.llvm.org/llvm.sh && \
     rm llvm.sh
 
 USER vscode
-RUN opam init --bare
 
 RUN rustup install stable
 
 RUN curl -fsSL https://gh.io/copilot-install | bash
 
-RUN opam option depext-run-installs=true
-ENV OPAMYES=1
-RUN --mount=type=bind,source=.git,destination=/c2p-repo \
-    git config --global --add safe.directory /c2p-repo && \
-    sudo mkdir /workspaces && sudo chown vscode:vscode /workspaces && \
-    cd /workspaces && git clone --depth=1 --recurse-submodules --reference-if-able=/c2p-repo --dissociate /c2p-repo c2pulse && \
-    cd c2pulse && \
-    ./opt/fstar/.scripts/get_fstar_z3.sh ~/.local/bin/ && \
-    make -j`nproc` build-pulse && \
-    sudo tar --zstd -cf /c2pulse-opt-cache.tar.zst opt .git/modules && \
-    cd / && sudo rm -rf /workspaces
+COPY ./opt/install-fstar.sh /tmp
+RUN /tmp/install-fstar.sh && sudo rm /tmp/install-fstar.sh

.devcontainer/devcontainer.json

@@ -1,6 +1,9 @@
 {
   "name": "c2pulse devcontainer",
-  "image": "ghcr.io/fstarlang/c2pulse-devcontainer",
+  "build": {
+    "context": "..",
+    "dockerfile": "Containerfile"
+  },
   "customizations": {
     "vscode": {
       "extensions": [
@@ -14,7 +17,6 @@
   },
   // Runs only once when container is prepared
   "onCreateCommand": {
-    "restore-opt-cache": "cd /workspaces/c2pulse && test ! -f opt/opam.done && tar -xf /c2pulse-opt-cache.tar.zst || echo not using cache"
   },
   // Runs periodically and/or when content of repo changes
   "updateContentCommand": {

.github/workflows/ci.yml

@@ -12,46 +12,6 @@ jobs:
     runs-on: ubuntu-latest
     steps:
     - uses: actions/checkout@v3
-      with:
-        submodules: recursive
-
-    - name: Install opam
-      run: |
-        sudo apt update
-        sudo apt install -y opam
-        opam init --bare
-
-    - name: Install Z3
-      run: |
-        echo "PATH=/usr/local/bin/:$PATH" >> $GITHUB_ENV
-        sudo ./opt/fstar/.scripts/get_fstar_z3.sh /usr/local/bin/
-
-    - name: Compute cache key
-      id: cachekey
-      run: |
-        echo "cachekey=$(./opt/ci-deps-hash)" >> "$GITHUB_OUTPUT"
-
-    - name: Get cache
-      id: getcache
-      uses: actions/cache/restore@v4
-      with:
-        path: opt
-        key: ${{ steps.cachekey.outputs.cachekey }}
-
-    - name: Restore changes to files in opt
-      run: |
-        git reset --hard
-
-    - name: Build dependencies
-      run: |
-        make -j$(nproc) build-pulse
-
-    - name: Save cache
-      if: ${{ steps.getcache.outputs.cache-hit != 'true' }}
-      uses: actions/cache/save@v4
-      with:
-        path: opt
-        key: ${{ steps.cachekey.outputs.cachekey }}
 
     - name: Install clang
       run: |
@@ -61,17 +21,13 @@ jobs:
         sudo apt update
         sudo apt install -y clang-20 libclang-cpp20-dev g++ clang-tools-20 libclang-20-dev
 
+    - name: Install F*
+      run: ./opt/install-fstar.sh --link-dir /usr/local/bin
+
     - name: Build c2pulse
       run: |
         make -j$(nproc)
 
     - name: Test c2pulse
       run: |
         make -j$(nproc) test
-
-    - name: Checking that code is correctly formatted
-      if: always()
-      run: |
-        cargo fmt
-        clang-format -i cpp/impl.cpp
-        git diff --exit-code

.github/workflows/copilot-setup-steps.yml

@@ -15,51 +15,14 @@ jobs:
 
     steps:
     - uses: actions/checkout@v3
-      with:
-        submodules: recursive
-
-    - name: Install opam
-      run: |
-        sudo apt update
-        sudo apt install -y opam
-        opam init --bare
-
-    - name: Install Z3
-      run: |
-        echo "PATH=/usr/local/bin/:$PATH" >> $GITHUB_ENV
-        sudo ./opt/fstar/.scripts/get_fstar_z3.sh /usr/local/bin/
-
-    - name: Compute cache key
-      id: cachekey
-      run: |
-        echo "cachekey=$(./opt/ci-deps-hash)" >> "$GITHUB_OUTPUT"
-
-    - name: Get cache
-      id: getcache
-      uses: actions/cache/restore@v4
-      with:
-        path: opt
-        key: ${{ steps.cachekey.outputs.cachekey }}
-
-    - name: Restore changes to files in opt
-      run: |
-        git reset --hard
-
-    - name: Build dependencies
-      run: |
-        make -j$(nproc) build-pulse
-
-    - name: Save cache
-      if: ${{ steps.getcache.outputs.cache-hit != 'true' }}
-      uses: actions/cache/save@v4
-      with:
-        path: opt
-        key: ${{ steps.cachekey.outputs.cachekey }}
 
     - name: Install clang
       run: |
         wget https://apt.llvm.org/llvm.sh
         chmod +x llvm.sh
         sudo ./llvm.sh 20
         sudo apt update
-        sudo apt install -y clang-20 libclang-cpp20-dev g++ clang-tools-20 libclang-20-dev
+        sudo apt install -y clang-20 libclang-cpp20-dev g++ clang-tools-20 libclang-20-dev
+
+    - name: Install F*
+      run: ./opt/install-fstar.sh --link-dir /usr/local/bin

.github/workflows/devcontainer.yml

@@ -5,53 +5,8 @@ all: rust lib
 rust:
 	cargo build
 
-ifeq ($(C2PULSE_OPT),0)
-
-opt/opam-available.done:
-	touch $@
-
-else
-
-opt/opam-available.done: opt/opam-init.done
-	touch $@
-
-opt/opam-init.done:
-	opam update
-	opam init --no-setup --root=opt/opam --compiler=5.3.0
-	touch $@
-
-endif
-
-opt/env.mk opt/env.sh: opt/opam-available.done
-	./opt/configure
-
-include opt/env.mk
-
-ifeq ($(C2PULSE_OPT),0)
-
-.PHONY: build-pulse
-build-pulse:
-
-else
-
-.PHONY: build-opam
-build-opam: opt/opam.done
-
-opt/opam.done: opt/fstar/fstar.opam
-	opam install --deps-only $<
-	touch $@
-
-.PHONY: build-fstar
-build-fstar: opt/opam.done
-	$(MAKE) -C opt/fstar ADMIT=1
-
-.PHONY: build-pulse
-build-pulse: build-fstar
-
-endif
-
 .PHONY: lib
-lib: build-pulse
+lib:
 	$(MAKE) -C pulse
 
 .PHONY: -testsuite