[Agda] Getting Agda building and running on Windows

[Aaron Gray]

Hi,

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 0.2.6.2 and agda
standard library 0.7 and 1.7.1 :-

    https://github.com/AaronNGray/docker-agda-stdlib

I am getting the following :-

     => ERROR [builder 11/13] RUN agda --verbose=0 src/Everything.agda
                                          142.1s
    ------
     > [builder 11/13] RUN agda --verbose=0 src/Everything.agda:
    #15 142.0
/root/.agda/lib/standard-library/src/Codata/Musical/Notation.agda:11,1-44
    #15 142.0 Importing module Agda.Builtin.Coinduction using the
--guardedness
    #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
--
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>