[Agda] Getting Agda building and running on Windows
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
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 0.2.6.2 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 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.
Independent Open Source Software Engineer, Computer Language Researcher,
and amateur computer scientist.
-------------- next part --------------
An HTML attachment was scrubbed...
More information about the Agda