[Agda] Getting Agda building and running on Windows

[Anton Setzer]

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/

Anton

________________________________
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,

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<https://eur03.safelinks.protection.outlook.com/?url=https%3A%2F%2Fgithub.com%2FAaronNGray%2Fdocker-agda-stdlib&data=04%7C01%7CA.G.Setzer%40Swansea.ac.uk%7C24acb3542b4a40d82ea108d9cfd1fbd5%7Cbbcab52e9fbe43d6a2f39f66c43df268%7C0%7C0%7C637769323461737818%7CUnknown%7CTWFpbGZsb3d8eyJWIjoiMC4wLjAwMDAiLCJQIjoiV2luMzIiLCJBTiI6Ik1haWwiLCJXVCI6Mn0%3D%7C2000&sdata=6%2BIY7b9midNtbC6MwQ1Bm%2B3DUI4NiH4E5SH5YGqJxm0%3D&reserved=0>

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