add minimal initial impl #32
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| name: why3-image | |
| on: | |
| push: | |
| branches: | |
| - main | |
| - update-why3-image | |
| paths: | |
| - infra/reference-env/** | |
| workflow_dispatch: | |
| permissions: | |
| contents: read | |
| packages: write | |
| concurrency: | |
| group: why3-image | |
| cancel-in-progress: true | |
| jobs: | |
| build-and-push: | |
| name: build and push | |
| runs-on: ubuntu-24.04 | |
| steps: | |
| - uses: actions/checkout@d23441a48e516b6c34aea4fa41551a30e30af803 | |
| - name: Log in to GHCR | |
| uses: docker/login-action@af1e73f918a031802d376d3c8bbc3fe56130a9b0 | |
| with: | |
| registry: ghcr.io | |
| username: ${{ github.actor }} | |
| password: ${{ secrets.GITHUB_TOKEN }} | |
| - name: Set up Docker Buildx | |
| uses: docker/setup-buildx-action@bb05f3f5519dd87d3ba754cc423b652a5edd6d2c | |
| - name: Build and push reference environment | |
| id: build | |
| uses: docker/build-push-action@53b7df96c91f9c12dcc8a07bcb9ccacbed38856a | |
| with: | |
| context: infra/reference-env | |
| platforms: linux/amd64 | |
| push: true | |
| tags: | | |
| ghcr.io/${{ github.repository }}-why3:1.7.2-z3-4.8.12 | |
| ghcr.io/${{ github.repository }}-why3:reference-env-${{ github.sha }} | |
| build-args: | | |
| OCAML_VERSION=4.14.4 | |
| WHY3_VERSION=1.7.2 | |
| WHY3_COMMIT=1343338d3bb1941c0d4f134283bb0790816113c4 | |
| WHY3_TREE=f5e82693620413d7d8e3ebcba69addcb6a65f877 | |
| WHY3_SOURCE_ARCHIVE_SHA256=c7bf782933a5d8ef9e78638cbf18e480eef895dca95317ba50231f20d45e92c7 | |
| Z3_VERSION=4.8.12 | |
| Z3_ARCHIVE_SHA256=648e8a7afb57445440ad711b733bd675e3888da2767c14ae5122582c924d8d52 | |
| REFERENCE_MANIFEST_SHA256=d842c4413353e620a6ee409f58cef8f5572db7e3d0a6dd50c007981f44fee2eb | |
| cache-from: type=gha,scope=why3-reference-env-v1 | |
| cache-to: type=gha,mode=max,scope=why3-reference-env-v1 | |
| - name: Verify pinned components and required Why3 capabilities | |
| env: | |
| IMAGE_DIGEST: ${{ steps.build.outputs.digest }} | |
| run: | | |
| image_ref="ghcr.io/${GITHUB_REPOSITORY}-why3@${IMAGE_DIGEST}" | |
| docker pull "$image_ref" | |
| docker run --rm --platform linux/amd64 "$image_ref" bash -ceu ' | |
| test "$(ocamlc -version)" = 4.14.4 | |
| test "$(why3 --version)" = "Why3 platform, version 1.7.2" | |
| test "$(z3 --version)" = "Z3 version 4.8.12 - 64 bit" | |
| printf "theory Simple\n goal trivial : true\nend\n" \ | |
| > /tmp/why3-sexp-smoke.mlw | |
| why3 pp --output=sexp /tmp/why3-sexp-smoke.mlw \ | |
| > /tmp/why3-sexp-smoke.sexp | |
| test -s /tmp/why3-sexp-smoke.sexp | |
| printf "%s %s\n" \ | |
| c7bf782933a5d8ef9e78638cbf18e480eef895dca95317ba50231f20d45e92c7 \ | |
| /opt/reference-env/why3-source.tar.gz \ | |
| | sha256sum --check --strict | |
| printf "let _ = Driver.prepare_task_trace\n" > /tmp/trace_probe.ml | |
| if ocamlfind ocamlc -package why3 -c /tmp/trace_probe.ml >/dev/null 2>&1; then | |
| echo "global Why3 unexpectedly contains the repository trace extension" >&2 | |
| exit 1 | |
| fi | |
| ' | |
| - name: Generate the environment lock candidate | |
| env: | |
| IMAGE_DIGEST: ${{ steps.build.outputs.digest }} | |
| run: | | |
| image_ref="ghcr.io/${GITHUB_REPOSITORY}-why3@${IMAGE_DIGEST}" | |
| container_id="$(docker create --platform linux/amd64 "$image_ref")" | |
| docker cp "$container_id:/opt/reference-env/manifest.json" \ | |
| "$RUNNER_TEMP/reference-env-manifest.json" | |
| docker rm "$container_id" | |
| node tools/why3_reference/generate_environment_lock_candidate.mjs \ | |
| --image-digest "$IMAGE_DIGEST" \ | |
| --manifest "$RUNNER_TEMP/reference-env-manifest.json" \ | |
| --output "$RUNNER_TEMP/reference-environment-lock-v1.json" | |
| - name: Report immutable image digest | |
| env: | |
| IMAGE_DIGEST: ${{ steps.build.outputs.digest }} | |
| run: | | |
| { | |
| echo '### Reference environment candidate' | |
| echo | |
| echo "Image digest: \`${IMAGE_DIGEST}\`" | |
| echo | |
| echo 'Promotion replaces only `tools/contracts/reference-environment-lock-v1.json`.' | |
| } >> "$GITHUB_STEP_SUMMARY" | |
| - name: Upload environment lock candidate | |
| uses: actions/upload-artifact@043fb46d1a93c77aae656e7c1c64a875d1fc6a0a | |
| with: | |
| name: reference-environment-${{ github.sha }} | |
| path: | | |
| ${{ runner.temp }}/reference-env-manifest.json | |
| ${{ runner.temp }}/reference-environment-lock-v1.json | |
| if-no-files-found: error | |
| retention-days: 30 |