nixosTests.agda: Adapt to --guardedness requirements

The one-line test is hard to fix in a readable manner
and doesn't really add value above the hello-world test.
So rather simplify to reduce maintenance.
This commit is contained in:
Manuel Bärenz 2021-07-15 08:47:25 +02:00 committed by sterni
parent 27ff64e919
commit 65fcd698bb

View file

@ -2,6 +2,7 @@ import ./make-test-python.nix ({ pkgs, ... }:
let
hello-world = pkgs.writeText "hello-world" ''
{-# OPTIONS --guardedness #-}
open import IO
open import Level
@ -35,10 +36,6 @@ in
machine.succeed("touch TestEmpty.agda")
machine.succeed("agda TestEmpty.agda")
# Minimal script that actually uses the standard library
machine.succeed('echo "import IO" > TestIO.agda')
machine.succeed("agda -l standard-library -i . TestIO.agda")
# Hello world
machine.succeed(
"cp ${hello-world} HelloWorld.agda"