Skip to content

Add and strengthen theorems #3937

Add and strengthen theorems

Add and strengthen theorems #3937

Workflow file for this run

---
name: Tests
on: [push, pull_request]
jobs:
build:
name: Build
runs-on: ubuntu-latest # container actions require GNU/Linux
strategy:
matrix:
coq_container:
# - coqorg/coq:8.12.2
# - coqorg/coq:8.16.1-ocaml-4.13.1-flambda
- coqorg/coq:8.18.0-ocaml-4.13.1-flambda
container:
image: ${{ matrix.coq_container }}
options: --user root
steps:
- uses: actions/checkout@v4
with:
persist-credentials: false
- name: Fix permissions
run: chown -R 1000 .
- name: ls
run: ls -la .
- name: Install Opam dependencies
run: su coq -c 'eval $(opam env) && opam install --deps-only --with-test --with-doc -y -j 2 ./Formal_ML.opam'
- name: Build using Make
run: su coq -c 'eval $(opam env) && make -kj 2'
- name: Build documentation
run: su coq -c 'eval $(opam env) && make -kj 2 doc'
# - uses: coq-community/docker-coq-action@v1
# with:
# opam_file: 'Formal_ML.opam'
# coq_version: ${{ matrix.coq_version }}
# ocaml_version: ${{ matrix.ocaml_version }}
# # export: 'OPAMWITHTEST OPAMWITHDOC'
# export: 'OPAMWITHDOC'
# after_script: |
# sudo cp -a $(opam config var Formal_ML:build)/documentation .
# env:
# OPAMWITHDOC: 'true'
# OPAMWITHTEST: 'true'
# - if: ${{ github.event_name == 'push' && github.ref == 'refs/heads/master' }}
# name: deploy documentation
# uses: JamesIves/[email protected]
# with:
# ACCESS_TOKEN: ${{ secrets.ACCESS_TOKEN }}
# REPOSITORY_NAME: FormalML/FormalML.github.io # the target repository
# TARGET_FOLDER: main/documentation # target directory
# BRANCH: main # The branch the action should deploy to.
# FOLDER: documentation # The folder the action should deploy.
# CLEAN: true # Automatically remove deleted files from the deploy branch