[Agda] Getting Agda building and running on Windows

Anton Setzer a.g.setzer at swansea.ac.uk
Fri Jan 7 03:30:27 CET 2022

Installing Agda using WSL worked for me very well. However, I needed to put all agda files including the standard library into the root directory (not into ~/  but into a folder in  / ) then the preformance is quite good. However you need to get a GUI running so that you have the emacs menus (which under Windows 11 will be provided which hopefully makes life easier, under Windows 10 you have to set it up yourself), I succeeded under windows 10 using vcXsrv, but that's a bit of work, documentation is not very good since it's quite new.  Maybe upgrading to Windows 11 first is a smart move.

For windows native installation the only success my students had was using Aaron Strump's installers under http://homepage.cs.uiowa.edu/~astump/agda/


From: Agda <agda-bounces at lists.chalmers.se> on behalf of Aaron Gray <aaronngray.lists at gmail.com>
Sent: 04 January 2022 22:31
To: agda at lists.chalmers.se <agda at lists.chalmers.se>
Subject: [Agda] Getting Agda building and running on Windows


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                                               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 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/20220107/0b564316/attachment.html>

More information about the Agda mailing list