Unverified Commit d1983f34 authored by Naïm Camille Favier's avatar Naïm Camille Favier Committed by GitHub
Browse files

agda: parameterize agda infrastructure by Agda executable name (#452961)

parents d766fcf7 55ac814f

ci/OWNERS

+1 −1
Original line number Diff line number Diff line
@@ -343,7 +343,7 @@ pkgs/development/python-modules/buildcatrust/ @ajs124 @lukegb @mweinelt 
/pkgs/top-level/agda-packages.nix         @NixOS/agda

/pkgs/development/libraries/agda          @NixOS/agda

/doc/languages-frameworks/agda.section.md @NixOS/agda

/nixos/tests/agda.nix                     @NixOS/agda

/nixos/tests/agda                         @NixOS/agda



# Idris

/pkgs/development/idris-modules @Infinisil

maintainers/maintainer-list.nix

+5 −0
Original line number Diff line number Diff line
@@ -4254,6 +4254,11 @@ 
    githubId = 498906;

    name = "Karolis Stasaitis";

  };

  carlostome = {

    name = "Carlos Tomé Cortiñas";

    github = "carlostome";

    githubId = 2206578;

  };

  carlsverre = {

    email = "accounts@carlsverre.com";

    github = "carlsverre";

nixos/tests/agda.nix→nixos/tests/agda/base.nix

+5 −7
Original line number Diff line number Diff line 
{ pkgs, ... }:



let

  hello-world = pkgs.writeText "hello-world" ''

    {-# OPTIONS --guardedness #-}

    open import IO

    open import Level



    main = run {0ℓ} (putStrLn "Hello World!")

  '';

  hello-world = ./files/HelloWorld.agda;

in

{

  name = "agda";
@@ -30,6 +24,10 @@ in 
    };



  testScript = ''

    # agda and agda-mode are in path

    machine.succeed("agda --version")

    machine.succeed("agda-mode")



    # Minimal script that typechecks

    machine.succeed("touch TestEmpty.agda")

    machine.succeed("agda TestEmpty.agda")

nixos/tests/agda/default.nix

0 → 100644
+5 −0
Original line number Diff line number Diff line 
{ runTest }:

{

  base = runTest ./base.nix;

  override-with-backend = runTest ./override-with-backend.nix;

}

nixos/tests/agda/files/HelloWorld.agda

0 → 100644
+5 −0
Original line number Diff line number Diff line 
{-# OPTIONS --guardedness #-}

open import IO

open import Level



main = run {0ℓ} (putStrLn "Hello World!")