Skip to content
hs-to-coq

Add GHC.Maybe edits in tests #100

Sign in to view logs

Add GHC.Maybe edits in tests

Add GHC.Maybe edits in tests #100

Workflow file for this run

.github/workflows/hs-to-coq.yml at b48f979
name: hs-to-coq
on: [push, pull_request]
jobs:
pre_check:
runs-on: ubuntu-latest
outputs:
should_skip_coq: ${{ steps.skip_coq_check.outputs.should_skip }}
should_skip_hs: ${{ steps.skip_hs_check.outputs.should_skip }}
steps:
- id: skip_hs_check
name: Check if the changes are about Haskell src files
uses: fkirc/skip-duplicate-actions@master
with:
paths: '["src/**", "stack.yaml", "hs-to-coq.cabal", "cabal.project"]'
- id: skip_coq_check
name: Check if the changes are about Coq files
uses: fkirc/skip-duplicate-actions@master
with:
paths: '["examples/**", "base/**", "base-thy/**"]'
installing-haskell:
name: Installing Haskell dependencies
runs-on: ${{ matrix.os }}
strategy:
matrix:
os: [ubuntu-latest]
ghc: [8.4.3]
resolver: [lts-12.0]
needs: pre_check
if: ${{ needs.pre_check.outputs.should_skip_hs != 'true' }}
steps:
- uses: actions/checkout@v2
- name: Caching Stack
id: caching-stack
uses: actions/cache@v2
with:
path: |
~/.stack
.stack-work
examples/containers/extraction/.stack-work
~/.ghc
key: stack-${{ runner.os }}-ghc${{ matrix.ghc }}-${{ matrix.resolver }}-${{ hashFiles('**/hs-to-coq.cabal') }}
- uses: haskell/actions/setup@v1
if: steps.caching-stack.outputs.cache-hit != 'true'
with:
ghc-version: ${{ matrix.ghc }}
enable-stack: true
stack-version: 'latest'
- name: Setup Stack
if: steps.caching-stack.outputs.cache-hit != 'true'
run: |
stack --no-terminal --install-ghc test --only-dependencies
stack --no-terminal --install-ghc install QuickCheck HUnit test-framework test-framework-hunit test-framework-quickcheck2
- name: Build hs-to-coq
if: steps.caching-stack.outputs.cache-hit != 'true'
run: stack --no-terminal --install-ghc build
installing-coq:
name: Installing Coq dependencies
runs-on: ${{ matrix.os }}
strategy:
matrix:
os: [ubuntu-latest]
ocaml: [4.07.1]
coq: [8.10.2]
needs: pre_check
if: ${{ needs.pre_check.outputs.should_skip_coq != 'true' }}
steps:
- name: Caching OPAM
id: caching-opam
uses: actions/cache@v2
with:
path: ~/.opam
key: opam-${{ runner.os }}-coq${{ matrix.coq }}
- name: Set up OCaml
if: steps.caching-opam.outputs.cache-hit != 'true'
uses: avsm/setup-ocaml@v1
with:
ocaml-version: ${{ matrix.ocaml }}
- name: Set up Coq
if: steps.caching-opam.outputs.cache-hit != 'true'
run: |
if ! [ -e $HOME/.opam/config ]; then opam init -j 2 -n -y; fi
opam repo add coq-released http://coq.inria.fr/opam/released || true
opam list -i coq.8.10.2 --silent || { opam update && opam unpin coq && opam install -v -y -j 1 --unlock-base coq.8.10.2 ocamlfind.1.8.0 ; }
opam list -i coq-mathcomp-ssreflect --silent || opam install -y coq-mathcomp-ssreflect
opam install -y coq-equations.1.2+8.10
cross-build-hs-to-coq:
name: Cross building hs-to-coq with multiple GHC versions
runs-on: ${{ matrix.os }}
strategy:
matrix:
os: [ubuntu-latest]
ghc: [8.4.3]
resolver: [lts-12.26, lts-14.27, lts-16.31, lts-18.10]
needs: pre_check
if: ${{ needs.pre_check.outputs.should_skip_hs != 'true' }}
steps:
- uses: actions/checkout@v2
- name: Caching Stack
id: caching-stack
uses: actions/cache@v2
with:
path: |
~/.stack
.stack-work
examples/containers/extraction/.stack-work
~/.ghc
key: stack-${{ runner.os }}-ghc${{ matrix.ghc }}-${{ matrix.resolver }}-${{ hashFiles('**/hs-to-coq.cabal') }}
- uses: haskell/actions/setup@v1
with:
ghc-version: ${{ matrix.ghc }}
enable-stack: true
stack-version: 'latest'
- name: Replacing resolver
run: sed -i 's/lts-.*/${{ matrix.resolver }}/g' stack.yaml
- name: Building hs-to-coq
run: |
stack --no-terminal --install-ghc test --only-dependencies
stack --no-terminal --install-ghc install QuickCheck HUnit test-framework test-framework-hunit test-framework-quickcheck2
stack --no-terminal --install-ghc build
test-coq-files:
name: Testing base, containers, transformers, GHC, etc.
runs-on: ${{ matrix.os }}
needs: [installing-coq, pre_check]
strategy:
matrix:
os: [ubuntu-latest]
ocaml: [4.07.1]
coq: [8.10.2]
if: ${{ needs.pre_check.outputs.should_skip_coq != 'true' }}
steps:
- uses: actions/checkout@v2
- name: Caching OPAM
uses: actions/cache@v2
with:
path: ~/.opam
key: opam-${{ runner.os }}-coq${{ matrix.coq }}
- name: Set up OCaml
uses: avsm/setup-ocaml@v1
with:
ocaml-version: ${{ matrix.ocaml }}
- name: Set up Coq
if: steps.caching-opam.outputs.cache-hit != 'true'
run: |
opam init -j 2 -n -y
- name: Installing Coq dependencies
run: |
opam repo add coq-released http://coq.inria.fr/opam/released || true
opam list -i coq.8.10.2 --silent || { opam update && opam unpin coq && opam install -v -y -j 1 --unlock-base coq.8.10.2 ocamlfind.1.8.0 ; }
opam list -i coq-mathcomp-ssreflect --silent || opam install -y coq-mathcomp-ssreflect
opam install -y coq-equations.1.2+8.10
- name: Compiling base
run: |
eval $(opam config env)
(cd base; coq_makefile -f _CoqProject -o Makefile)
make -j -C base
(cd base-thy; coq_makefile -f _CoqProject -o Makefile)
make -j -C base-thy
- name: Compiling transformers
run: |
eval $(opam config env)
(cd examples/transformers/lib; coq_makefile -f _CoqProject -o Makefile)
make -j -C examples/transformers/lib
(cd examples/transformers/theories; coq_makefile -f _CoqProject -o Makefile)
make -j -C examples/transformers/theories
- name: Compiling containers
run: |
eval $(opam config env)
(cd examples/containers/lib; coq_makefile -f _CoqProject -o Makefile)
make -j -C examples/containers/lib
(cd examples/containers/theories; coq_makefile -f _CoqProject -o Makefile)
make -j -C examples/containers/theories
- name: Compiling GHC and core-semantics
run: |
eval $(opam config env)
(cd examples/ghc/lib; coq_makefile -f _CoqProject -o Makefile)
make -j -C examples/ghc/lib
(cd examples/ghc/theories; coq_makefile -f _CoqProject -o Makefile)
make -j -C examples/ghc/theories
(cd examples/core-semantics/lib; coq_makefile -f _CoqProject -o Makefile)
make -j -C examples/core-semantics/lib
- name: Compiling Graph (FGL)
run: |
eval $(opam config env)
(cd examples/graph/lib; coq_makefile -f _CoqProject -o Makefile)
make -j -C examples/graph/lib
(cd examples/graph/theories; coq_makefile -f _CoqProject -o Makefile)
make -j -C examples/graph/theories
tests:
name: Tests, base tests, and other examples
runs-on: ${{ matrix.os }}
needs: [installing-haskell, installing-coq, pre_check]
if: ${{ needs.pre_check.outputs.should_skip_coq != 'true' && needs.pre_check.outputs.should_skip_hs != 'true' }}
strategy:
matrix:
os: [ubuntu-latest]
ghc: [8.4.3]
resolver: [lts-12.0]
ocaml: [4.07.1]
coq: [8.10.2]
steps:
- uses: actions/checkout@v2
- uses: haskell/actions/setup@v1
with:
ghc-version: ${{ matrix.ghc }}
enable-stack: true
stack-version: 'latest'
- name: Caching Stack
uses: actions/cache@v2
with:
path: |
~/.stack
.stack-work
examples/containers/extraction/.stack-work
~/.ghc
key: stack-${{ runner.os }}-ghc${{ matrix.ghc }}-${{ matrix.resolver }}-${{ hashFiles('**/hs-to-coq.cabal') }}
- name: Setup Stack
if: steps.caching-stack.outputs.cache-hit != 'true'
run: |
stack --no-terminal --install-ghc test --only-dependencies
stack --no-terminal --install-ghc install QuickCheck HUnit test-framework test-framework-hunit test-framework-quickcheck2
- name: Build hs-to-coq
run: stack --no-terminal --install-ghc build
- name: Caching OPAM
uses: actions/cache@v2
with:
path: ~/.opam
key: opam-${{ runner.os }}-coq${{ matrix.coq }}
- name: Set up OPAM
uses: avsm/setup-ocaml@v1
with:
ocaml-version: ${{ matrix.ocaml }}
- name: Set up Coq
if: steps.caching-opam.outputs.cache-hit != 'true'
run: |
opam init -j 2 -n -y
- name: Installing Coq dependencies
run: |
opam repo add coq-released http://coq.inria.fr/opam/released || true
opam list -i coq.8.10.2 --silent || { opam update && opam unpin coq && opam install -v -y -j 1 --unlock-base coq.8.10.2 ocamlfind.1.8.0 ; }
opam list -i coq-mathcomp-ssreflect --silent || opam install -y coq-mathcomp-ssreflect
opam install -y coq-equations.1.2+8.10
- name: Run tests
run: |
eval $(opam config env)
(cd base; coq_makefile -f _CoqProject -o Makefile)
make -j -C base
make -j -C examples/tests
make -j -C examples/base-tests
(cd base-thy; coq_makefile -f _CoqProject -o Makefile)
make -j -C base-thy
make -j -C examples/successors
make -j -C examples/compiler
make -j -C examples/rle
make -j -C examples/bag
make -j -C examples/quicksort
make -j -C examples/dlist
make -j -C examples/intervals
make -j -C examples/coinduction
test-translation:
name: Translation (ensures convenience copy is up-to-date)
runs-on: ${{ matrix.os }}
needs: [installing-haskell, pre_check]
strategy:
matrix:
os: [ubuntu-latest]
ghc: [8.4.3]
resolver: [lts-12.0]
ocaml: [4.07.1]
coq: [8.10.2]
if: ${{ needs.pre_check.outputs.should_skip_hs != 'true' }}
steps:
- uses: actions/checkout@v2
with:
submodules: recursive
- name: Installing dependencies for Linux
if: runner.os == 'Linux'
run: sudo apt-get install xutils-dev
- name: Installing dependencies for MacOS
if: runner.os == 'macOS'
run: |
brew install --cask xquartz
export PATH=$PATH:/usr/X11/bin >> ~/.bash_profile
- uses: haskell/actions/setup@v1
with:
ghc-version: ${{ matrix.ghc }}
enable-stack: true
stack-version: 'latest'
- name: Caching Stack
uses: actions/cache@v2
with:
path: |
~/.stack
.stack-work
examples/containers/extraction/.stack-work
~/.ghc
key: stack-${{ runner.os }}-ghc${{ matrix.ghc }}-${{ matrix.resolver }}-${{ hashFiles('**/hs-to-coq.cabal') }}
- name: Setup Stack
if: steps.caching-stack.outputs.cache-hit != 'true'
run: |
stack --no-terminal --install-ghc test --only-dependencies
stack --no-terminal --install-ghc install QuickCheck HUnit test-framework test-framework-hunit test-framework-quickcheck2
- name: Build hs-to-coq
run: stack --no-terminal --install-ghc build
- name: Translating base
run: |
make -C examples/base-src clean
make -C examples/base-src vfiles
- name: Comparing convenience copy of base
run: |
git add base
git status
git diff-index --cached --quiet HEAD -- base
- name: Translating containers
run: |
make -C examples/containers clean
make -C examples/containers vfiles
- name: Comparing convenience copy of containers
run: |
git add examples/containers/lib
git status
git diff-index --cached --quiet HEAD -- examples/containers/lib
- name: Translating transformers
run: |
make -C examples/transformers clean
make -C examples/transformers vfiles
- name: Comparing convenience copy of transformers
run: |
git add examples/transformers/lib
git status
git diff-index --cached --quiet HEAD -- examples/transformers/lib
- name: Translating GHC and core-semantics
run: |
make -C examples/ghc clean
make -C examples/ghc vfiles
make -C examples/core-semantics clean
make -C examples/core-semantics vfiles
- name: Comparing convenience copy of GHC and core-semantics
run: |
git add examples/ghc/lib
git add examples/core-semantics/lib
git status
git diff-index --cached --quiet HEAD -- examples/ghc/lib/
- name: Translating Graph (FGL)
run: |
make -C examples/graph clean
make -C examples/graph vfiles
- name: Comparing convenience copy of Graph (FGL)
run: |
git add examples/graph/lib
git status
git diff-index --cached --quiet HEAD -- examples/graph/lib
test-container-extraction:
name: Testing containers extraction
runs-on: ${{ matrix.os }}
needs: [installing-haskell, installing-coq, pre_check]
strategy:
matrix:
os: [ubuntu-latest]
ghc: [8.4.3]
resolver: [lts-12.0]
ocaml: [4.07.1]
coq: [8.10.2]
if: ${{ needs.pre_check.outputs.should_skip_coq != 'true' }}
steps:
- uses: actions/checkout@v2
with:
submodules: recursive
- uses: haskell/actions/setup@v1
with:
ghc-version: ${{ matrix.ghc }}
enable-stack: true
stack-version: 'latest'
- name: Caching Stack
uses: actions/cache@v2
with:
path: |
~/.stack
.stack-work
examples/containers/extraction/.stack-work
~/.ghc
key: stack-${{ runner.os }}-ghc${{ matrix.ghc }}-${{ matrix.resolver }}-${{ hashFiles('**/hs-to-coq.cabal') }}
- name: Setup Stack
if: steps.caching-stack.outputs.cache-hit != 'true'
run: |
stack --no-terminal --install-ghc test --only-dependencies
stack --no-terminal --install-ghc install QuickCheck HUnit test-framework test-framework-hunit test-framework-quickcheck2
- name: Build hs-to-coq
run: stack --no-terminal --install-ghc build
- name: Caching OPAM
uses: actions/cache@v2
with:
path: ~/.opam
key: opam-${{ runner.os }}-coq${{ matrix.coq }}
- name: Set up OPAM
uses: avsm/setup-ocaml@v1
with:
ocaml-version: ${{ matrix.ocaml }}
- name: Set up Coq
if: steps.caching-opam.outputs.cache-hit != 'true'
run: |
opam init -j 2 -n -y
- name: Installing Coq dependencies
run: |
opam repo add coq-released http://coq.inria.fr/opam/released || true
opam list -i coq.8.10.2 --silent || { opam update && opam unpin coq && opam install -v -y -j 1 --unlock-base coq.8.10.2 ocamlfind.1.8.0 ; }
opam list -i coq-mathcomp-ssreflect --silent || opam install -y coq-mathcomp-ssreflect
opam install -y coq-equations.1.2+8.10
- name: Extract containers
run: |
stack --no-terminal --install-ghc build
eval $(opam config env)
(cd base; coq_makefile -f _CoqProject -o Makefile)
make -j2 -C base
(cd examples/containers/lib; coq_makefile -f _CoqProject -o Makefile)
make -j2 -C examples/containers/lib
(cd examples/containers/extraction/extracted-src; coq_makefile -f _CoqProject -o Makefile)
make -j2 -C examples/containers/extraction/extracted-src/
perl -i examples/containers/extraction/extracted-src/fixcode.pl examples/containers/extraction/extracted-src/*.hs
- name: Testing containers extraction
run: |
cd examples/containers/extraction
stack --no-terminal --install-ghc test
- name: Bench
run: stack --no-terminal --install-ghc bench