<div dir="ltr">Hi,<br><br>Hi, I am a Agda newbie and trying to get a working platform on Windows.<div><br><div>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 !<br><br>Is there a standard Docker script for Agda ?<br><br>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.<div><br></div><div>Its working upto failing on Agda Standard Library, something to do with 

--guardedness in Codata/Musical/Notation.agda<br><br>I have updated an existing Docker script to support Agda 0.2.6.2 and agda standard library 0.7 and 1.7.1 :-<br><br>    <a href="https://github.com/AaronNGray/docker-agda-stdlib">https://github.com/AaronNGray/docker-agda-stdlib</a><div><br></div><div>I am getting the following :-</div><div><br></div><div>     => ERROR [builder 11/13] RUN agda --verbose=0 src/Everything.agda                                               142.1s<br>    ------<br>     > [builder 11/13] RUN agda --verbose=0 src/Everything.agda:<br>    #15 142.0 /root/.agda/lib/standard-library/src/Codata/Musical/Notation.agda:11,1-44<br>    #15 142.0 Importing module Agda.Builtin.Coinduction using the --guardedness<br>    #15 142.0 flag from a module which does not.<br>    #15 142.0 when scope checking the declaration<br>    #15 142.0   open import Agda.Builtin.Coinduction public<br>    ------<br>    executor failed running [/bin/sh -c agda --verbose=0 src/Everything.agda]: exit code: 42</div><div><br></div><div>Any help would be appreciated.</div><div><br></div><div><div>Aaron</div><div>--<br></div><div>Aaron Gray<br><br>Independent Open Source Software Engineer, Computer Language Researcher, and amateur computer scientist.</div></div></div></div></div></div>