[Agda] Getting Agda building and running on Windows

Aaron Gray aaronngray.lists at gmail.com
Tue Jan 4 23:31:18 CET 2022


Hi, I am a Agda newbie and trying to get a working platform on Windows.

I have tried Ubuntu on WLS on Windows 10, versions are well old, why I
don't know, Chocolatey, issues with Agda Standard Library and now trying
Docker !

Is there a standard Docker script for Agda ?

I tried a docker script that presumably I thought worked on older versions
but I have just found does not even get as far as I have.

Its working upto failing on Agda Standard Library, something to do with
--guardedness in Codata/Musical/Notation.agda

I have updated an existing Docker script to support Agda and agda
standard library 0.7 and 1.7.1 :-


I am getting the following :-

     => ERROR [builder 11/13] RUN agda --verbose=0 src/Everything.agda
     > [builder 11/13] RUN agda --verbose=0 src/Everything.agda:
    #15 142.0
    #15 142.0 Importing module Agda.Builtin.Coinduction using the
    #15 142.0 flag from a module which does not.
    #15 142.0 when scope checking the declaration
    #15 142.0   open import Agda.Builtin.Coinduction public
    executor failed running [/bin/sh -c agda --verbose=0
src/Everything.agda]: exit code: 42

Any help would be appreciated.

Aaron Gray

Independent Open Source Software Engineer, Computer Language Researcher,
and amateur computer scientist.
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.chalmers.se/pipermail/agda/attachments/20220104/a81393ea/attachment.html>

More information about the Agda mailing list