Skip to content

Commit

Permalink
This commit does not belong to any branch on this repository, and may belong to a fork outside of the repository.
Add test that Agda works in nix develop
Browse files Browse the repository at this point in the history
HeinrichApfelmus committed Nov 30, 2023
1 parent d381347 commit 5b8107e
Showing 4 changed files with 40 additions and 0 deletions.
17 changes: 17 additions & 0 deletions .buildkite/check-agda.sh
Original file line number Diff line number Diff line change
@@ -0,0 +1,17 @@
#!/usr/bin/env bash

set -euo pipefail

cd .buildkite/check-agda

echo "### Checking Agda"
agda \
--no-default-libraries \
--local-interfaces \
Everything.agda && rm Everything.agdai

echo "### Checking agda2hs"
agda2hs \
--no-default-libraries \
--local-interfaces \
Everything.agda && rm Everything.hs Everything.agdai
7 changes: 7 additions & 0 deletions .buildkite/check-agda/Everything.agda
Original file line number Diff line number Diff line change
@@ -0,0 +1,7 @@
module Everything where

-- standard-library
open import Data.Sum using (_⊎_; inj₁; inj₂)

-- agda2hs
open import Haskell.Prelude
6 changes: 6 additions & 0 deletions .buildkite/check-agda/check.agda-lib
Original file line number Diff line number Diff line change
@@ -0,0 +1,6 @@
name: check
include: .
depend:
standard-library
agda2hs
flags: -W noUnsupportedIndexedMatch --erasure
10 changes: 10 additions & 0 deletions .buildkite/pipeline.yml
Original file line number Diff line number Diff line change
@@ -47,6 +47,7 @@ steps:
system: ${linux}
env:
TMPDIR: "/cache"

- label: "Check cardano-ledger-specs"
depends_on: linux-nix
command: |
@@ -55,3 +56,12 @@ steps:
system: ${linux}
env:
TMPDIR: "/cache"

- label: "Check agda2hs"
depends_on: linux-nix
command: |
${nix} --command bash -c '.buildkite/check-agda.sh'
agents:
system: ${linux}
env:
TMPDIR: "/cache"

0 comments on commit 5b8107e

Please sign in to comment.