forked from auxolotl/docs
3061 lines
66 KiB
HTML
3061 lines
66 KiB
HTML
|
|
<!doctype html>
|
|
<html lang="en" class="no-js">
|
|
<head>
|
|
|
|
<meta charset="utf-8">
|
|
<meta name="viewport" content="width=device-width,initial-scale=1">
|
|
|
|
<meta name="description" content="Aux Documentation">
|
|
|
|
|
|
<meta name="author" content="Nixpkgs Aux, and Lix Contributors">
|
|
|
|
|
|
<link rel="canonical" href="https://docs.auxolotl.org/Nixpkgs/Languages-And-Frameworks/agda.section/">
|
|
|
|
|
|
<link rel="prev" href="../">
|
|
|
|
|
|
<link rel="next" href="../android.section/">
|
|
|
|
|
|
<link rel="icon" href="../../../assets/aux-logo.svg">
|
|
<meta name="generator" content="mkdocs-1.6.0, mkdocs-material-9.5.29">
|
|
|
|
|
|
|
|
<title>Agda - Aux Docs</title>
|
|
|
|
|
|
|
|
<link rel="stylesheet" href="../../../assets/stylesheets/main.76a95c52.min.css">
|
|
|
|
|
|
<link rel="stylesheet" href="../../../assets/stylesheets/palette.06af60db.min.css">
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
<link rel="preconnect" href="https://fonts.gstatic.com" crossorigin>
|
|
<link rel="stylesheet" href="https://fonts.bunny.net/css?family=IBM+Plex+Sans:300,300i,400,400i,700,700i%7CIBM+Plex+Mono:400,400i,700,700i&display=fallback">
|
|
<style>:root{--md-text-font:"IBM Plex Sans";--md-code-font:"IBM Plex Mono"}</style>
|
|
|
|
|
|
|
|
<script>__md_scope=new URL("../../..",location),__md_hash=e=>[...e].reduce((e,_)=>(e<<5)-e+_.charCodeAt(0),0),__md_get=(e,_=localStorage,t=__md_scope)=>JSON.parse(_.getItem(t.pathname+"."+e)),__md_set=(e,_,t=localStorage,a=__md_scope)=>{try{t.setItem(a.pathname+"."+e,JSON.stringify(_))}catch(e){}}</script>
|
|
|
|
|
|
|
|
|
|
|
|
|
|
<meta property="og:type" content="website" >
|
|
|
|
<meta property="og:title" content="Agda {#agda} - Aux Docs" >
|
|
|
|
<meta property="og:description" content="Aux Documentation" >
|
|
|
|
<meta property="og:image" content="https://docs.auxolotl.org/assets/images/social/Nixpkgs/Languages-And-Frameworks/agda.section.png" >
|
|
|
|
<meta property="og:image:type" content="image/png" >
|
|
|
|
<meta property="og:image:width" content="1200" >
|
|
|
|
<meta property="og:image:height" content="630" >
|
|
|
|
<meta property="og:url" content="https://docs.auxolotl.org/Nixpkgs/Languages-And-Frameworks/agda.section/" >
|
|
|
|
<meta name="twitter:card" content="summary_large_image" >
|
|
|
|
<meta name="twitter:title" content="Agda {#agda} - Aux Docs" >
|
|
|
|
<meta name="twitter:description" content="Aux Documentation" >
|
|
|
|
<meta name="twitter:image" content="https://docs.auxolotl.org/assets/images/social/Nixpkgs/Languages-And-Frameworks/agda.section.png" >
|
|
|
|
|
|
|
|
</head>
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
<body dir="ltr" data-md-color-scheme="default" data-md-color-primary="indigo" data-md-color-accent="blue">
|
|
|
|
|
|
<input class="md-toggle" data-md-toggle="drawer" type="checkbox" id="__drawer" autocomplete="off">
|
|
<input class="md-toggle" data-md-toggle="search" type="checkbox" id="__search" autocomplete="off">
|
|
<label class="md-overlay" for="__drawer"></label>
|
|
<div data-md-component="skip">
|
|
|
|
|
|
<a href="#agda" class="md-skip">
|
|
Skip to content
|
|
</a>
|
|
|
|
</div>
|
|
<div data-md-component="announce">
|
|
|
|
</div>
|
|
|
|
|
|
|
|
|
|
<header class="md-header" data-md-component="header">
|
|
<nav class="md-header__inner md-grid" aria-label="Header">
|
|
<a href="../../.." title="Aux Docs" class="md-header__button md-logo" aria-label="Aux Docs" data-md-component="logo">
|
|
|
|
<img src="../../../assets/aux-logo.svg" alt="logo">
|
|
|
|
</a>
|
|
<label class="md-header__button md-icon" for="__drawer">
|
|
|
|
<svg xmlns="http://www.w3.org/2000/svg" viewBox="0 0 24 24"><path d="M3 6h18v2H3V6m0 5h18v2H3v-2m0 5h18v2H3v-2Z"/></svg>
|
|
</label>
|
|
<div class="md-header__title" data-md-component="header-title">
|
|
<div class="md-header__ellipsis">
|
|
<div class="md-header__topic">
|
|
<span class="md-ellipsis">
|
|
Aux Docs
|
|
</span>
|
|
</div>
|
|
<div class="md-header__topic" data-md-component="header-topic">
|
|
<span class="md-ellipsis">
|
|
|
|
Agda
|
|
|
|
</span>
|
|
</div>
|
|
</div>
|
|
</div>
|
|
|
|
|
|
<form class="md-header__option" data-md-component="palette">
|
|
|
|
|
|
|
|
|
|
<input class="md-option" data-md-color-media="(prefers-color-scheme: light)" data-md-color-scheme="default" data-md-color-primary="indigo" data-md-color-accent="blue" aria-label="Dark Mode" type="radio" name="__palette" id="__palette_0">
|
|
|
|
<label class="md-header__button md-icon" title="Dark Mode" for="__palette_1" hidden>
|
|
<svg xmlns="http://www.w3.org/2000/svg" viewBox="0 0 24 24"><path d="m17.75 4.09-2.53 1.94.91 3.06-2.63-1.81-2.63 1.81.91-3.06-2.53-1.94L12.44 4l1.06-3 1.06 3 3.19.09m3.5 6.91-1.64 1.25.59 1.98-1.7-1.17-1.7 1.17.59-1.98L15.75 11l2.06-.05L18.5 9l.69 1.95 2.06.05m-2.28 4.95c.83-.08 1.72 1.1 1.19 1.85-.32.45-.66.87-1.08 1.27C15.17 23 8.84 23 4.94 19.07c-3.91-3.9-3.91-10.24 0-14.14.4-.4.82-.76 1.27-1.08.75-.53 1.93.36 1.85 1.19-.27 2.86.69 5.83 2.89 8.02a9.96 9.96 0 0 0 8.02 2.89m-1.64 2.02a12.08 12.08 0 0 1-7.8-3.47c-2.17-2.19-3.33-5-3.49-7.82-2.81 3.14-2.7 7.96.31 10.98 3.02 3.01 7.84 3.12 10.98.31Z"/></svg>
|
|
</label>
|
|
|
|
|
|
|
|
|
|
|
|
<input class="md-option" data-md-color-media="(prefers-color-scheme: dark)" data-md-color-scheme="slate" data-md-color-primary="indigo" data-md-color-accent="blue" aria-label="Light Mode" type="radio" name="__palette" id="__palette_1">
|
|
|
|
<label class="md-header__button md-icon" title="Light Mode" for="__palette_0" hidden>
|
|
<svg xmlns="http://www.w3.org/2000/svg" viewBox="0 0 24 24"><path d="M12 7a5 5 0 0 1 5 5 5 5 0 0 1-5 5 5 5 0 0 1-5-5 5 5 0 0 1 5-5m0 2a3 3 0 0 0-3 3 3 3 0 0 0 3 3 3 3 0 0 0 3-3 3 3 0 0 0-3-3m0-7 2.39 3.42C13.65 5.15 12.84 5 12 5c-.84 0-1.65.15-2.39.42L12 2M3.34 7l4.16-.35A7.2 7.2 0 0 0 5.94 8.5c-.44.74-.69 1.5-.83 2.29L3.34 7m.02 10 1.76-3.77a7.131 7.131 0 0 0 2.38 4.14L3.36 17M20.65 7l-1.77 3.79a7.023 7.023 0 0 0-2.38-4.15l4.15.36m-.01 10-4.14.36c.59-.51 1.12-1.14 1.54-1.86.42-.73.69-1.5.83-2.29L20.64 17M12 22l-2.41-3.44c.74.27 1.55.44 2.41.44.82 0 1.63-.17 2.37-.44L12 22Z"/></svg>
|
|
</label>
|
|
|
|
|
|
</form>
|
|
|
|
|
|
|
|
<script>var media,input,key,value,palette=__md_get("__palette");if(palette&&palette.color){"(prefers-color-scheme)"===palette.color.media&&(media=matchMedia("(prefers-color-scheme: light)"),input=document.querySelector(media.matches?"[data-md-color-media='(prefers-color-scheme: light)']":"[data-md-color-media='(prefers-color-scheme: dark)']"),palette.color.media=input.getAttribute("data-md-color-media"),palette.color.scheme=input.getAttribute("data-md-color-scheme"),palette.color.primary=input.getAttribute("data-md-color-primary"),palette.color.accent=input.getAttribute("data-md-color-accent"));for([key,value]of Object.entries(palette.color))document.body.setAttribute("data-md-color-"+key,value)}</script>
|
|
|
|
|
|
|
|
<label class="md-header__button md-icon" for="__search">
|
|
|
|
<svg xmlns="http://www.w3.org/2000/svg" viewBox="0 0 24 24"><path d="M9.5 3A6.5 6.5 0 0 1 16 9.5c0 1.61-.59 3.09-1.56 4.23l.27.27h.79l5 5-1.5 1.5-5-5v-.79l-.27-.27A6.516 6.516 0 0 1 9.5 16 6.5 6.5 0 0 1 3 9.5 6.5 6.5 0 0 1 9.5 3m0 2C7 5 5 7 5 9.5S7 14 9.5 14 14 12 14 9.5 12 5 9.5 5Z"/></svg>
|
|
</label>
|
|
<div class="md-search" data-md-component="search" role="dialog">
|
|
<label class="md-search__overlay" for="__search"></label>
|
|
<div class="md-search__inner" role="search">
|
|
<form class="md-search__form" name="search">
|
|
<input type="text" class="md-search__input" name="query" aria-label="Search" placeholder="Search" autocapitalize="off" autocorrect="off" autocomplete="off" spellcheck="false" data-md-component="search-query" required>
|
|
<label class="md-search__icon md-icon" for="__search">
|
|
|
|
<svg xmlns="http://www.w3.org/2000/svg" viewBox="0 0 24 24"><path d="M9.5 3A6.5 6.5 0 0 1 16 9.5c0 1.61-.59 3.09-1.56 4.23l.27.27h.79l5 5-1.5 1.5-5-5v-.79l-.27-.27A6.516 6.516 0 0 1 9.5 16 6.5 6.5 0 0 1 3 9.5 6.5 6.5 0 0 1 9.5 3m0 2C7 5 5 7 5 9.5S7 14 9.5 14 14 12 14 9.5 12 5 9.5 5Z"/></svg>
|
|
|
|
<svg xmlns="http://www.w3.org/2000/svg" viewBox="0 0 24 24"><path d="M20 11v2H8l5.5 5.5-1.42 1.42L4.16 12l7.92-7.92L13.5 5.5 8 11h12Z"/></svg>
|
|
</label>
|
|
<nav class="md-search__options" aria-label="Search">
|
|
|
|
<button type="reset" class="md-search__icon md-icon" title="Clear" aria-label="Clear" tabindex="-1">
|
|
|
|
<svg xmlns="http://www.w3.org/2000/svg" viewBox="0 0 24 24"><path d="M19 6.41 17.59 5 12 10.59 6.41 5 5 6.41 10.59 12 5 17.59 6.41 19 12 13.41 17.59 19 19 17.59 13.41 12 19 6.41Z"/></svg>
|
|
</button>
|
|
</nav>
|
|
|
|
</form>
|
|
<div class="md-search__output">
|
|
<div class="md-search__scrollwrap" tabindex="0" data-md-scrollfix>
|
|
<div class="md-search-result" data-md-component="search-result">
|
|
<div class="md-search-result__meta">
|
|
Initializing search
|
|
</div>
|
|
<ol class="md-search-result__list" role="presentation"></ol>
|
|
</div>
|
|
</div>
|
|
</div>
|
|
</div>
|
|
</div>
|
|
|
|
|
|
<div class="md-header__source">
|
|
<a href="https://git.auxolotl.org/auxolotl/docs" title="Go to repository" class="md-source" data-md-component="source">
|
|
<div class="md-source__icon md-icon">
|
|
|
|
<svg xmlns="http://www.w3.org/2000/svg" viewBox="0 0 24 24"><path d="M16.777 0a2.9 2.9 0 1 1-2.529 4.322H12.91a4.266 4.266 0 0 0-4.265 4.195v2.118a7.076 7.076 0 0 1 4.147-1.42l.118-.002h1.338a2.9 2.9 0 0 1 5.43 1.422 2.9 2.9 0 0 1-5.43 1.422H12.91a4.266 4.266 0 0 0-4.265 4.195v2.319A2.9 2.9 0 0 1 7.222 24 2.9 2.9 0 0 1 5.8 18.57V8.589a7.109 7.109 0 0 1 6.991-7.108l.118-.001h1.338A2.9 2.9 0 0 1 16.778 0ZM7.223 19.905a1.194 1.194 0 1 0 0 2.389 1.194 1.194 0 0 0 0-2.389Zm9.554-10.464a1.194 1.194 0 1 0 0 2.389 1.194 1.194 0 0 0 0-2.39Zm0-7.735a1.194 1.194 0 1 0 0 2.389 1.194 1.194 0 0 0 0-2.389Z"/></svg>
|
|
</div>
|
|
<div class="md-source__repository">
|
|
auxolotl/docs
|
|
</div>
|
|
</a>
|
|
</div>
|
|
|
|
</nav>
|
|
|
|
</header>
|
|
|
|
<div class="md-container" data-md-component="container">
|
|
|
|
|
|
|
|
|
|
|
|
<nav class="md-tabs" aria-label="Tabs" data-md-component="tabs">
|
|
<div class="md-grid">
|
|
<ul class="md-tabs__list">
|
|
|
|
|
|
|
|
|
|
|
|
<li class="md-tabs__item">
|
|
<a href="../../.." class="md-tabs__link">
|
|
|
|
|
|
|
|
|
|
Aux Documentation Hub
|
|
|
|
</a>
|
|
</li>
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
<li class="md-tabs__item">
|
|
<a href="../../../TODO/" class="md-tabs__link">
|
|
|
|
|
|
|
|
|
|
TODO
|
|
|
|
</a>
|
|
</li>
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
<li class="md-tabs__item">
|
|
<a href="../../../Aux/" class="md-tabs__link">
|
|
|
|
|
|
|
|
|
|
Aux
|
|
|
|
</a>
|
|
</li>
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
<li class="md-tabs__item">
|
|
<a href="../../../Lix/" class="md-tabs__link">
|
|
|
|
|
|
|
|
|
|
Lix
|
|
|
|
</a>
|
|
</li>
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
<li class="md-tabs__item">
|
|
<a href="../../../NixOS/appstream/" class="md-tabs__link">
|
|
|
|
|
|
|
|
|
|
NixOS
|
|
|
|
</a>
|
|
</li>
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
<li class="md-tabs__item md-tabs__item--active">
|
|
<a href="../../" class="md-tabs__link">
|
|
|
|
|
|
|
|
|
|
Nixpkgs
|
|
|
|
</a>
|
|
</li>
|
|
|
|
|
|
|
|
|
|
</ul>
|
|
</div>
|
|
</nav>
|
|
|
|
|
|
|
|
<main class="md-main" data-md-component="main">
|
|
<div class="md-main__inner md-grid">
|
|
|
|
|
|
|
|
<div class="md-sidebar md-sidebar--primary" data-md-component="sidebar" data-md-type="navigation" >
|
|
<div class="md-sidebar__scrollwrap">
|
|
<div class="md-sidebar__inner">
|
|
|
|
|
|
|
|
|
|
|
|
|
|
<nav class="md-nav md-nav--primary md-nav--lifted" aria-label="Navigation" data-md-level="0">
|
|
<label class="md-nav__title" for="__drawer">
|
|
<a href="../../.." title="Aux Docs" class="md-nav__button md-logo" aria-label="Aux Docs" data-md-component="logo">
|
|
|
|
<img src="../../../assets/aux-logo.svg" alt="logo">
|
|
|
|
</a>
|
|
Aux Docs
|
|
</label>
|
|
|
|
<div class="md-nav__source">
|
|
<a href="https://git.auxolotl.org/auxolotl/docs" title="Go to repository" class="md-source" data-md-component="source">
|
|
<div class="md-source__icon md-icon">
|
|
|
|
<svg xmlns="http://www.w3.org/2000/svg" viewBox="0 0 24 24"><path d="M16.777 0a2.9 2.9 0 1 1-2.529 4.322H12.91a4.266 4.266 0 0 0-4.265 4.195v2.118a7.076 7.076 0 0 1 4.147-1.42l.118-.002h1.338a2.9 2.9 0 0 1 5.43 1.422 2.9 2.9 0 0 1-5.43 1.422H12.91a4.266 4.266 0 0 0-4.265 4.195v2.319A2.9 2.9 0 0 1 7.222 24 2.9 2.9 0 0 1 5.8 18.57V8.589a7.109 7.109 0 0 1 6.991-7.108l.118-.001h1.338A2.9 2.9 0 0 1 16.778 0ZM7.223 19.905a1.194 1.194 0 1 0 0 2.389 1.194 1.194 0 0 0 0-2.389Zm9.554-10.464a1.194 1.194 0 1 0 0 2.389 1.194 1.194 0 0 0 0-2.39Zm0-7.735a1.194 1.194 0 1 0 0 2.389 1.194 1.194 0 0 0 0-2.389Z"/></svg>
|
|
</div>
|
|
<div class="md-source__repository">
|
|
auxolotl/docs
|
|
</div>
|
|
</a>
|
|
</div>
|
|
|
|
<ul class="md-nav__list" data-md-scrollfix>
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
<li class="md-nav__item">
|
|
<a href="../../.." class="md-nav__link">
|
|
|
|
|
|
<span class="md-ellipsis">
|
|
Aux Documentation Hub
|
|
</span>
|
|
|
|
|
|
</a>
|
|
</li>
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
<li class="md-nav__item">
|
|
<a href="../../../TODO/" class="md-nav__link">
|
|
|
|
|
|
<span class="md-ellipsis">
|
|
TODO
|
|
</span>
|
|
|
|
|
|
</a>
|
|
</li>
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
<li class="md-nav__item md-nav__item--pruned md-nav__item--nested">
|
|
|
|
|
|
|
|
|
|
<a href="../../../Aux/" class="md-nav__link">
|
|
|
|
|
|
<span class="md-ellipsis">
|
|
Aux
|
|
</span>
|
|
|
|
|
|
|
|
<span class="md-nav__icon md-icon"></span>
|
|
|
|
</a>
|
|
|
|
|
|
|
|
</li>
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
<li class="md-nav__item md-nav__item--pruned md-nav__item--nested">
|
|
|
|
|
|
|
|
|
|
<a href="../../../Lix/" class="md-nav__link">
|
|
|
|
|
|
<span class="md-ellipsis">
|
|
Lix
|
|
</span>
|
|
|
|
|
|
|
|
<span class="md-nav__icon md-icon"></span>
|
|
|
|
</a>
|
|
|
|
|
|
|
|
</li>
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
<li class="md-nav__item md-nav__item--pruned md-nav__item--nested">
|
|
|
|
|
|
|
|
|
|
<a href="../../../NixOS/appstream/" class="md-nav__link">
|
|
|
|
|
|
<span class="md-ellipsis">
|
|
NixOS
|
|
</span>
|
|
|
|
|
|
|
|
<span class="md-nav__icon md-icon"></span>
|
|
|
|
</a>
|
|
|
|
|
|
|
|
</li>
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
<li class="md-nav__item md-nav__item--active md-nav__item--section md-nav__item--nested">
|
|
|
|
|
|
|
|
<input class="md-nav__toggle md-toggle " type="checkbox" id="__nav_6" checked>
|
|
|
|
|
|
|
|
<div class="md-nav__link md-nav__container">
|
|
<a href="../../" class="md-nav__link ">
|
|
|
|
|
|
<span class="md-ellipsis">
|
|
Nixpkgs
|
|
</span>
|
|
|
|
|
|
</a>
|
|
|
|
|
|
<label class="md-nav__link " for="__nav_6" id="__nav_6_label" tabindex="">
|
|
<span class="md-nav__icon md-icon"></span>
|
|
</label>
|
|
|
|
</div>
|
|
|
|
<nav class="md-nav" data-md-level="1" aria-labelledby="__nav_6_label" aria-expanded="true">
|
|
<label class="md-nav__title" for="__nav_6">
|
|
<span class="md-nav__icon md-icon"></span>
|
|
Nixpkgs
|
|
</label>
|
|
<ul class="md-nav__list" data-md-scrollfix>
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
<li class="md-nav__item">
|
|
<a href="../../options/" class="md-nav__link">
|
|
|
|
|
|
<span class="md-ellipsis">
|
|
Options
|
|
</span>
|
|
|
|
|
|
</a>
|
|
</li>
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
<li class="md-nav__item md-nav__item--pruned md-nav__item--nested">
|
|
|
|
|
|
|
|
|
|
<a href="../../Build-Helpers/" class="md-nav__link">
|
|
|
|
|
|
<span class="md-ellipsis">
|
|
Build Helpers
|
|
</span>
|
|
|
|
|
|
|
|
<span class="md-nav__icon md-icon"></span>
|
|
|
|
</a>
|
|
|
|
|
|
|
|
</li>
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
<li class="md-nav__item md-nav__item--pruned md-nav__item--nested">
|
|
|
|
|
|
|
|
|
|
<a href="../../Development/" class="md-nav__link">
|
|
|
|
|
|
<span class="md-ellipsis">
|
|
Development
|
|
</span>
|
|
|
|
|
|
|
|
<span class="md-nav__icon md-icon"></span>
|
|
|
|
</a>
|
|
|
|
|
|
|
|
</li>
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
<li class="md-nav__item md-nav__item--pruned md-nav__item--nested">
|
|
|
|
|
|
|
|
|
|
<a href="../../Functions/" class="md-nav__link">
|
|
|
|
|
|
<span class="md-ellipsis">
|
|
Functions
|
|
</span>
|
|
|
|
|
|
|
|
<span class="md-nav__icon md-icon"></span>
|
|
|
|
</a>
|
|
|
|
|
|
|
|
</li>
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
<li class="md-nav__item md-nav__item--pruned md-nav__item--nested">
|
|
|
|
|
|
|
|
|
|
<a href="../../Hooks/" class="md-nav__link">
|
|
|
|
|
|
<span class="md-ellipsis">
|
|
Hooks
|
|
</span>
|
|
|
|
|
|
|
|
<span class="md-nav__icon md-icon"></span>
|
|
|
|
</a>
|
|
|
|
|
|
|
|
</li>
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
<li class="md-nav__item md-nav__item--active md-nav__item--nested">
|
|
|
|
|
|
|
|
<input class="md-nav__toggle md-toggle " type="checkbox" id="__nav_6_7" checked>
|
|
|
|
|
|
|
|
<div class="md-nav__link md-nav__container">
|
|
<a href="../" class="md-nav__link ">
|
|
|
|
|
|
<span class="md-ellipsis">
|
|
Languages And Frameworks
|
|
</span>
|
|
|
|
|
|
</a>
|
|
|
|
|
|
<label class="md-nav__link " for="__nav_6_7" id="__nav_6_7_label" tabindex="0">
|
|
<span class="md-nav__icon md-icon"></span>
|
|
</label>
|
|
|
|
</div>
|
|
|
|
<nav class="md-nav" data-md-level="2" aria-labelledby="__nav_6_7_label" aria-expanded="true">
|
|
<label class="md-nav__title" for="__nav_6_7">
|
|
<span class="md-nav__icon md-icon"></span>
|
|
Languages And Frameworks
|
|
</label>
|
|
<ul class="md-nav__list" data-md-scrollfix>
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
<li class="md-nav__item md-nav__item--active">
|
|
|
|
<input class="md-nav__toggle md-toggle" type="checkbox" id="__toc">
|
|
|
|
|
|
|
|
|
|
|
|
<label class="md-nav__link md-nav__link--active" for="__toc">
|
|
|
|
|
|
<span class="md-ellipsis">
|
|
Agda
|
|
</span>
|
|
|
|
|
|
<span class="md-nav__icon md-icon"></span>
|
|
</label>
|
|
|
|
<a href="./" class="md-nav__link md-nav__link--active">
|
|
|
|
|
|
<span class="md-ellipsis">
|
|
Agda
|
|
</span>
|
|
|
|
|
|
</a>
|
|
|
|
|
|
|
|
<nav class="md-nav md-nav--secondary" aria-label="Table of contents">
|
|
|
|
|
|
|
|
|
|
|
|
|
|
<label class="md-nav__title" for="__toc">
|
|
<span class="md-nav__icon md-icon"></span>
|
|
Table of contents
|
|
</label>
|
|
<ul class="md-nav__list" data-md-component="toc" data-md-scrollfix>
|
|
|
|
<li class="md-nav__item">
|
|
<a href="#how-to-use-agda" class="md-nav__link">
|
|
<span class="md-ellipsis">
|
|
How to use Agda
|
|
</span>
|
|
</a>
|
|
|
|
</li>
|
|
|
|
<li class="md-nav__item">
|
|
<a href="#compiling-agda" class="md-nav__link">
|
|
<span class="md-ellipsis">
|
|
Compiling Agda
|
|
</span>
|
|
</a>
|
|
|
|
</li>
|
|
|
|
<li class="md-nav__item">
|
|
<a href="#writing-agda-packages" class="md-nav__link">
|
|
<span class="md-ellipsis">
|
|
Writing Agda packages
|
|
</span>
|
|
</a>
|
|
|
|
<nav class="md-nav" aria-label="Writing Agda packages">
|
|
<ul class="md-nav__list">
|
|
|
|
<li class="md-nav__item">
|
|
<a href="#building-agda-packages" class="md-nav__link">
|
|
<span class="md-ellipsis">
|
|
Building Agda packages
|
|
</span>
|
|
</a>
|
|
|
|
</li>
|
|
|
|
<li class="md-nav__item">
|
|
<a href="#installing-agda-packages" class="md-nav__link">
|
|
<span class="md-ellipsis">
|
|
Installing Agda packages
|
|
</span>
|
|
</a>
|
|
|
|
</li>
|
|
|
|
</ul>
|
|
</nav>
|
|
|
|
</li>
|
|
|
|
<li class="md-nav__item">
|
|
<a href="#maintaining-the-agda-package-set-on-nixpkgs" class="md-nav__link">
|
|
<span class="md-ellipsis">
|
|
Maintaining the Agda package set on Nixpkgs
|
|
</span>
|
|
</a>
|
|
|
|
<nav class="md-nav" aria-label="Maintaining the Agda package set on Nixpkgs">
|
|
<ul class="md-nav__list">
|
|
|
|
<li class="md-nav__item">
|
|
<a href="#adding-agda-packages-to-nixpkgs" class="md-nav__link">
|
|
<span class="md-ellipsis">
|
|
Adding Agda packages to Nixpkgs
|
|
</span>
|
|
</a>
|
|
|
|
</li>
|
|
|
|
<li class="md-nav__item">
|
|
<a href="#agda-maintaining-packages" class="md-nav__link">
|
|
<span class="md-ellipsis">
|
|
Maintaining Agda packages
|
|
</span>
|
|
</a>
|
|
|
|
</li>
|
|
|
|
</ul>
|
|
</nav>
|
|
|
|
</li>
|
|
|
|
</ul>
|
|
|
|
</nav>
|
|
|
|
</li>
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
<li class="md-nav__item">
|
|
<a href="../android.section/" class="md-nav__link">
|
|
|
|
|
|
<span class="md-ellipsis">
|
|
Android
|
|
</span>
|
|
|
|
|
|
</a>
|
|
</li>
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
<li class="md-nav__item">
|
|
<a href="../beam.section/" class="md-nav__link">
|
|
|
|
|
|
<span class="md-ellipsis">
|
|
BEAM Languages (Erlang, Elixir & LFE)
|
|
</span>
|
|
|
|
|
|
</a>
|
|
</li>
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
<li class="md-nav__item">
|
|
<a href="../bower.section/" class="md-nav__link">
|
|
|
|
|
|
<span class="md-ellipsis">
|
|
Bower
|
|
</span>
|
|
|
|
|
|
</a>
|
|
</li>
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
<li class="md-nav__item">
|
|
<a href="../chicken.section/" class="md-nav__link">
|
|
|
|
|
|
<span class="md-ellipsis">
|
|
CHICKEN
|
|
</span>
|
|
|
|
|
|
</a>
|
|
</li>
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
<li class="md-nav__item">
|
|
<a href="../coq.section/" class="md-nav__link">
|
|
|
|
|
|
<span class="md-ellipsis">
|
|
Coq and coq packages
|
|
</span>
|
|
|
|
|
|
</a>
|
|
</li>
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
<li class="md-nav__item">
|
|
<a href="../crystal.section/" class="md-nav__link">
|
|
|
|
|
|
<span class="md-ellipsis">
|
|
Crystal
|
|
</span>
|
|
|
|
|
|
</a>
|
|
</li>
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
<li class="md-nav__item">
|
|
<a href="../cuda.section/" class="md-nav__link">
|
|
|
|
|
|
<span class="md-ellipsis">
|
|
CUDA
|
|
</span>
|
|
|
|
|
|
</a>
|
|
</li>
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
<li class="md-nav__item">
|
|
<a href="../cuelang.section/" class="md-nav__link">
|
|
|
|
|
|
<span class="md-ellipsis">
|
|
Cue (Cuelang)
|
|
</span>
|
|
|
|
|
|
</a>
|
|
</li>
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
<li class="md-nav__item">
|
|
<a href="../dart.section/" class="md-nav__link">
|
|
|
|
|
|
<span class="md-ellipsis">
|
|
Dart
|
|
</span>
|
|
|
|
|
|
</a>
|
|
</li>
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
<li class="md-nav__item">
|
|
<a href="../dhall.section/" class="md-nav__link">
|
|
|
|
|
|
<span class="md-ellipsis">
|
|
Dhall
|
|
</span>
|
|
|
|
|
|
</a>
|
|
</li>
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
<li class="md-nav__item">
|
|
<a href="../dlang.section/" class="md-nav__link">
|
|
|
|
|
|
<span class="md-ellipsis">
|
|
D (Dlang)
|
|
</span>
|
|
|
|
|
|
</a>
|
|
</li>
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
<li class="md-nav__item">
|
|
<a href="../dotnet.section/" class="md-nav__link">
|
|
|
|
|
|
<span class="md-ellipsis">
|
|
Dotnet
|
|
</span>
|
|
|
|
|
|
</a>
|
|
</li>
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
<li class="md-nav__item">
|
|
<a href="../emscripten.section/" class="md-nav__link">
|
|
|
|
|
|
<span class="md-ellipsis">
|
|
Emscripten
|
|
</span>
|
|
|
|
|
|
</a>
|
|
</li>
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
<li class="md-nav__item">
|
|
<a href="../gnome.section/" class="md-nav__link">
|
|
|
|
|
|
<span class="md-ellipsis">
|
|
GNOME
|
|
</span>
|
|
|
|
|
|
</a>
|
|
</li>
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
<li class="md-nav__item">
|
|
<a href="../go.section/" class="md-nav__link">
|
|
|
|
|
|
<span class="md-ellipsis">
|
|
Go
|
|
</span>
|
|
|
|
|
|
</a>
|
|
</li>
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
<li class="md-nav__item">
|
|
<a href="../gradle.section/" class="md-nav__link">
|
|
|
|
|
|
<span class="md-ellipsis">
|
|
Gradle
|
|
</span>
|
|
|
|
|
|
</a>
|
|
</li>
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
<li class="md-nav__item">
|
|
<a href="../hare.section/" class="md-nav__link">
|
|
|
|
|
|
<span class="md-ellipsis">
|
|
Hare
|
|
</span>
|
|
|
|
|
|
</a>
|
|
</li>
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
<li class="md-nav__item">
|
|
<a href="../haskell.section/" class="md-nav__link">
|
|
|
|
|
|
<span class="md-ellipsis">
|
|
Haskell
|
|
</span>
|
|
|
|
|
|
</a>
|
|
</li>
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
<li class="md-nav__item">
|
|
<a href="../hy.section/" class="md-nav__link">
|
|
|
|
|
|
<span class="md-ellipsis">
|
|
Hy
|
|
</span>
|
|
|
|
|
|
</a>
|
|
</li>
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
<li class="md-nav__item">
|
|
<a href="../idris.section/" class="md-nav__link">
|
|
|
|
|
|
<span class="md-ellipsis">
|
|
Idris
|
|
</span>
|
|
|
|
|
|
</a>
|
|
</li>
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
<li class="md-nav__item">
|
|
<a href="../idris2.section/" class="md-nav__link">
|
|
|
|
|
|
<span class="md-ellipsis">
|
|
Idris2
|
|
</span>
|
|
|
|
|
|
</a>
|
|
</li>
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
<li class="md-nav__item">
|
|
<a href="../ios.section/" class="md-nav__link">
|
|
|
|
|
|
<span class="md-ellipsis">
|
|
iOS
|
|
</span>
|
|
|
|
|
|
</a>
|
|
</li>
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
<li class="md-nav__item">
|
|
<a href="../java.section/" class="md-nav__link">
|
|
|
|
|
|
<span class="md-ellipsis">
|
|
Java
|
|
</span>
|
|
|
|
|
|
</a>
|
|
</li>
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
<li class="md-nav__item">
|
|
<a href="../javascript.section/" class="md-nav__link">
|
|
|
|
|
|
<span class="md-ellipsis">
|
|
Javascript
|
|
</span>
|
|
|
|
|
|
</a>
|
|
</li>
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
<li class="md-nav__item">
|
|
<a href="../julia.section/" class="md-nav__link">
|
|
|
|
|
|
<span class="md-ellipsis">
|
|
Julia
|
|
</span>
|
|
|
|
|
|
</a>
|
|
</li>
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
<li class="md-nav__item">
|
|
<a href="../lisp.section/" class="md-nav__link">
|
|
|
|
|
|
<span class="md-ellipsis">
|
|
lisp-modules
|
|
</span>
|
|
|
|
|
|
</a>
|
|
</li>
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
<li class="md-nav__item">
|
|
<a href="../lua.section/" class="md-nav__link">
|
|
|
|
|
|
<span class="md-ellipsis">
|
|
Lua
|
|
</span>
|
|
|
|
|
|
</a>
|
|
</li>
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
<li class="md-nav__item">
|
|
<a href="../maven.section/" class="md-nav__link">
|
|
|
|
|
|
<span class="md-ellipsis">
|
|
Maven
|
|
</span>
|
|
|
|
|
|
</a>
|
|
</li>
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
<li class="md-nav__item">
|
|
<a href="../nim.section/" class="md-nav__link">
|
|
|
|
|
|
<span class="md-ellipsis">
|
|
Nim
|
|
</span>
|
|
|
|
|
|
</a>
|
|
</li>
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
<li class="md-nav__item">
|
|
<a href="../ocaml.section/" class="md-nav__link">
|
|
|
|
|
|
<span class="md-ellipsis">
|
|
OCaml
|
|
</span>
|
|
|
|
|
|
</a>
|
|
</li>
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
<li class="md-nav__item">
|
|
<a href="../octave.section/" class="md-nav__link">
|
|
|
|
|
|
<span class="md-ellipsis">
|
|
Octave
|
|
</span>
|
|
|
|
|
|
</a>
|
|
</li>
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
<li class="md-nav__item">
|
|
<a href="../perl.section/" class="md-nav__link">
|
|
|
|
|
|
<span class="md-ellipsis">
|
|
Perl
|
|
</span>
|
|
|
|
|
|
</a>
|
|
</li>
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
<li class="md-nav__item">
|
|
<a href="../php.section/" class="md-nav__link">
|
|
|
|
|
|
<span class="md-ellipsis">
|
|
PHP
|
|
</span>
|
|
|
|
|
|
</a>
|
|
</li>
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
<li class="md-nav__item">
|
|
<a href="../pkg-config.section/" class="md-nav__link">
|
|
|
|
|
|
<span class="md-ellipsis">
|
|
pkg-config
|
|
</span>
|
|
|
|
|
|
</a>
|
|
</li>
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
<li class="md-nav__item">
|
|
<a href="../python.section/" class="md-nav__link">
|
|
|
|
|
|
<span class="md-ellipsis">
|
|
Python
|
|
</span>
|
|
|
|
|
|
</a>
|
|
</li>
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
<li class="md-nav__item">
|
|
<a href="../qt.section/" class="md-nav__link">
|
|
|
|
|
|
<span class="md-ellipsis">
|
|
Qt
|
|
</span>
|
|
|
|
|
|
</a>
|
|
</li>
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
<li class="md-nav__item">
|
|
<a href="../r.section/" class="md-nav__link">
|
|
|
|
|
|
<span class="md-ellipsis">
|
|
R
|
|
</span>
|
|
|
|
|
|
</a>
|
|
</li>
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
<li class="md-nav__item">
|
|
<a href="../ruby.section/" class="md-nav__link">
|
|
|
|
|
|
<span class="md-ellipsis">
|
|
Ruby
|
|
</span>
|
|
|
|
|
|
</a>
|
|
</li>
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
<li class="md-nav__item">
|
|
<a href="../rust.section/" class="md-nav__link">
|
|
|
|
|
|
<span class="md-ellipsis">
|
|
Rust
|
|
</span>
|
|
|
|
|
|
</a>
|
|
</li>
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
<li class="md-nav__item">
|
|
<a href="../scheme.section/" class="md-nav__link">
|
|
|
|
|
|
<span class="md-ellipsis">
|
|
Scheme
|
|
</span>
|
|
|
|
|
|
</a>
|
|
</li>
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
<li class="md-nav__item">
|
|
<a href="../swift.section/" class="md-nav__link">
|
|
|
|
|
|
<span class="md-ellipsis">
|
|
Swift
|
|
</span>
|
|
|
|
|
|
</a>
|
|
</li>
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
<li class="md-nav__item">
|
|
<a href="../texlive.section/" class="md-nav__link">
|
|
|
|
|
|
<span class="md-ellipsis">
|
|
TeX Live
|
|
</span>
|
|
|
|
|
|
</a>
|
|
</li>
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
<li class="md-nav__item">
|
|
<a href="../titanium.section/" class="md-nav__link">
|
|
|
|
|
|
<span class="md-ellipsis">
|
|
Titanium
|
|
</span>
|
|
|
|
|
|
</a>
|
|
</li>
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
<li class="md-nav__item">
|
|
<a href="../vim.section/" class="md-nav__link">
|
|
|
|
|
|
<span class="md-ellipsis">
|
|
Vim
|
|
</span>
|
|
|
|
|
|
</a>
|
|
</li>
|
|
|
|
|
|
|
|
|
|
</ul>
|
|
</nav>
|
|
|
|
</li>
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
<li class="md-nav__item md-nav__item--pruned md-nav__item--nested">
|
|
|
|
|
|
|
|
|
|
<a href="../../Library-Reference/asserts/" class="md-nav__link">
|
|
|
|
|
|
<span class="md-ellipsis">
|
|
Library Reference
|
|
</span>
|
|
|
|
|
|
|
|
<span class="md-nav__icon md-icon"></span>
|
|
|
|
</a>
|
|
|
|
|
|
|
|
</li>
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
<li class="md-nav__item md-nav__item--pruned md-nav__item--nested">
|
|
|
|
|
|
|
|
|
|
<a href="../../Module-System/module-system.chapter/" class="md-nav__link">
|
|
|
|
|
|
<span class="md-ellipsis">
|
|
Module System
|
|
</span>
|
|
|
|
|
|
|
|
<span class="md-nav__icon md-icon"></span>
|
|
|
|
</a>
|
|
|
|
|
|
|
|
</li>
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
<li class="md-nav__item md-nav__item--pruned md-nav__item--nested">
|
|
|
|
|
|
|
|
|
|
<a href="../../Packages/" class="md-nav__link">
|
|
|
|
|
|
<span class="md-ellipsis">
|
|
Packages
|
|
</span>
|
|
|
|
|
|
|
|
<span class="md-nav__icon md-icon"></span>
|
|
|
|
</a>
|
|
|
|
|
|
|
|
</li>
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
<li class="md-nav__item md-nav__item--pruned md-nav__item--nested">
|
|
|
|
|
|
|
|
|
|
<a href="../../Standard-Environment/" class="md-nav__link">
|
|
|
|
|
|
<span class="md-ellipsis">
|
|
Standard Environment
|
|
</span>
|
|
|
|
|
|
|
|
<span class="md-nav__icon md-icon"></span>
|
|
|
|
</a>
|
|
|
|
|
|
|
|
</li>
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
<li class="md-nav__item md-nav__item--pruned md-nav__item--nested">
|
|
|
|
|
|
|
|
|
|
<a href="../../Using-Nixpkgs/" class="md-nav__link">
|
|
|
|
|
|
<span class="md-ellipsis">
|
|
Using Nixpkgs
|
|
</span>
|
|
|
|
|
|
|
|
<span class="md-nav__icon md-icon"></span>
|
|
|
|
</a>
|
|
|
|
|
|
|
|
</li>
|
|
|
|
|
|
|
|
|
|
</ul>
|
|
</nav>
|
|
|
|
</li>
|
|
|
|
|
|
|
|
</ul>
|
|
</nav>
|
|
</div>
|
|
</div>
|
|
</div>
|
|
|
|
|
|
|
|
<div class="md-sidebar md-sidebar--secondary" data-md-component="sidebar" data-md-type="toc" >
|
|
<div class="md-sidebar__scrollwrap">
|
|
<div class="md-sidebar__inner">
|
|
|
|
|
|
<nav class="md-nav md-nav--secondary" aria-label="Table of contents">
|
|
|
|
|
|
|
|
|
|
|
|
|
|
<label class="md-nav__title" for="__toc">
|
|
<span class="md-nav__icon md-icon"></span>
|
|
Table of contents
|
|
</label>
|
|
<ul class="md-nav__list" data-md-component="toc" data-md-scrollfix>
|
|
|
|
<li class="md-nav__item">
|
|
<a href="#how-to-use-agda" class="md-nav__link">
|
|
<span class="md-ellipsis">
|
|
How to use Agda
|
|
</span>
|
|
</a>
|
|
|
|
</li>
|
|
|
|
<li class="md-nav__item">
|
|
<a href="#compiling-agda" class="md-nav__link">
|
|
<span class="md-ellipsis">
|
|
Compiling Agda
|
|
</span>
|
|
</a>
|
|
|
|
</li>
|
|
|
|
<li class="md-nav__item">
|
|
<a href="#writing-agda-packages" class="md-nav__link">
|
|
<span class="md-ellipsis">
|
|
Writing Agda packages
|
|
</span>
|
|
</a>
|
|
|
|
<nav class="md-nav" aria-label="Writing Agda packages">
|
|
<ul class="md-nav__list">
|
|
|
|
<li class="md-nav__item">
|
|
<a href="#building-agda-packages" class="md-nav__link">
|
|
<span class="md-ellipsis">
|
|
Building Agda packages
|
|
</span>
|
|
</a>
|
|
|
|
</li>
|
|
|
|
<li class="md-nav__item">
|
|
<a href="#installing-agda-packages" class="md-nav__link">
|
|
<span class="md-ellipsis">
|
|
Installing Agda packages
|
|
</span>
|
|
</a>
|
|
|
|
</li>
|
|
|
|
</ul>
|
|
</nav>
|
|
|
|
</li>
|
|
|
|
<li class="md-nav__item">
|
|
<a href="#maintaining-the-agda-package-set-on-nixpkgs" class="md-nav__link">
|
|
<span class="md-ellipsis">
|
|
Maintaining the Agda package set on Nixpkgs
|
|
</span>
|
|
</a>
|
|
|
|
<nav class="md-nav" aria-label="Maintaining the Agda package set on Nixpkgs">
|
|
<ul class="md-nav__list">
|
|
|
|
<li class="md-nav__item">
|
|
<a href="#adding-agda-packages-to-nixpkgs" class="md-nav__link">
|
|
<span class="md-ellipsis">
|
|
Adding Agda packages to Nixpkgs
|
|
</span>
|
|
</a>
|
|
|
|
</li>
|
|
|
|
<li class="md-nav__item">
|
|
<a href="#agda-maintaining-packages" class="md-nav__link">
|
|
<span class="md-ellipsis">
|
|
Maintaining Agda packages
|
|
</span>
|
|
</a>
|
|
|
|
</li>
|
|
|
|
</ul>
|
|
</nav>
|
|
|
|
</li>
|
|
|
|
</ul>
|
|
|
|
</nav>
|
|
</div>
|
|
</div>
|
|
</div>
|
|
|
|
|
|
|
|
<div class="md-content" data-md-component="content">
|
|
<article class="md-content__inner md-typeset">
|
|
|
|
|
|
|
|
|
|
<h1 id="agda">Agda</h1>
|
|
<h2 id="how-to-use-agda">How to use Agda</h2>
|
|
<p>Agda is available as the <a href="https://search.nixos.org/packages?channel=unstable&show=agda&from=0&size=30&sort=relevance&query=agda">agda</a>
|
|
package.</p>
|
|
<p>The <code>agda</code> package installs an Agda-wrapper, which calls <code>agda</code> with <code>--library-file</code>
|
|
set to a generated library-file within the nix store, this means your library-file in
|
|
<code>$HOME/.agda/libraries</code> will be ignored. By default the agda package installs Agda
|
|
with no libraries, i.e. the generated library-file is empty. To use Agda with libraries,
|
|
the <code>agda.withPackages</code> function can be used. This function either takes:</p>
|
|
<ul>
|
|
<li>A list of packages,</li>
|
|
<li>or a function which returns a list of packages when given the <code>agdaPackages</code> attribute set,</li>
|
|
<li>or an attribute set containing a list of packages and a GHC derivation for compilation (see below).</li>
|
|
<li>or an attribute set containing a function which returns a list of packages when given the <code>agdaPackages</code> attribute set and a GHC derivation for compilation (see below).</li>
|
|
</ul>
|
|
<p>For example, suppose we wanted a version of Agda which has access to the standard library. This can be obtained with the expressions:</p>
|
|
<div class="highlight"><pre><span></span><code>agda<span class="o">.</span>withPackages <span class="p">[</span> agdaPackages<span class="o">.</span>standard-library <span class="p">]</span>
|
|
</code></pre></div>
|
|
<p>or</p>
|
|
<div class="highlight"><pre><span></span><code>agda<span class="o">.</span>withPackages <span class="p">(</span>p<span class="p">:</span> <span class="p">[</span> p<span class="o">.</span>standard-library <span class="p">])</span>
|
|
</code></pre></div>
|
|
<p>or can be called as in the <a href="#compiling-agda">Compiling Agda</a> section.</p>
|
|
<p>If you want to use a different version of a library (for instance a development version)
|
|
override the <code>src</code> attribute of the package to point to your local repository</p>
|
|
<div class="highlight"><pre><span></span><code>agda<span class="o">.</span>withPackages <span class="p">(</span>p<span class="p">:</span> <span class="p">[</span>
|
|
<span class="p">(</span>p<span class="o">.</span>standard-library<span class="o">.</span>overrideAttrs <span class="p">(</span>oldAttrs<span class="p">:</span> <span class="p">{</span>
|
|
<span class="ss">version</span> <span class="o">=</span> <span class="s2">"local version"</span><span class="p">;</span>
|
|
<span class="ss">src</span> <span class="o">=</span> <span class="l">/path/to/local/repo/agda-stdlib</span><span class="p">;</span>
|
|
<span class="p">}))</span>
|
|
<span class="p">])</span>
|
|
</code></pre></div>
|
|
<p>You can also reference a GitHub repository</p>
|
|
<div class="highlight"><pre><span></span><code>agda<span class="o">.</span>withPackages <span class="p">(</span>p<span class="p">:</span> <span class="p">[</span>
|
|
<span class="p">(</span>p<span class="o">.</span>standard-library<span class="o">.</span>overrideAttrs <span class="p">(</span>oldAttrs<span class="p">:</span> <span class="p">{</span>
|
|
<span class="ss">version</span> <span class="o">=</span> <span class="s2">"1.5"</span><span class="p">;</span>
|
|
<span class="ss">src</span> <span class="o">=</span> fetchFromGitHub <span class="p">{</span>
|
|
<span class="ss">repo</span> <span class="o">=</span> <span class="s2">"agda-stdlib"</span><span class="p">;</span>
|
|
<span class="ss">owner</span> <span class="o">=</span> <span class="s2">"agda"</span><span class="p">;</span>
|
|
<span class="ss">rev</span> <span class="o">=</span> <span class="s2">"v1.5"</span><span class="p">;</span>
|
|
<span class="ss">hash</span> <span class="o">=</span> <span class="s2">"sha256-nEyxYGSWIDNJqBfGpRDLiOAnlHJKEKAOMnIaqfVZzJk="</span><span class="p">;</span>
|
|
<span class="p">};</span>
|
|
<span class="p">}))</span>
|
|
<span class="p">])</span>
|
|
</code></pre></div>
|
|
<p>If you want to use a library not added to Nixpkgs, you can add a
|
|
dependency to a local library by calling <code>agdaPackages.mkDerivation</code>.</p>
|
|
<div class="highlight"><pre><span></span><code>agda<span class="o">.</span>withPackages <span class="p">(</span>p<span class="p">:</span> <span class="p">[</span>
|
|
<span class="p">(</span>p<span class="o">.</span>mkDerivation <span class="p">{</span>
|
|
<span class="ss">pname</span> <span class="o">=</span> <span class="s2">"your-agda-lib"</span><span class="p">;</span>
|
|
<span class="ss">version</span> <span class="o">=</span> <span class="s2">"1.0.0"</span><span class="p">;</span>
|
|
<span class="ss">src</span> <span class="o">=</span> <span class="l">/path/to/your-agda-lib</span><span class="p">;</span>
|
|
<span class="p">})</span>
|
|
<span class="p">])</span>
|
|
</code></pre></div>
|
|
<p>Again you can reference GitHub</p>
|
|
<div class="highlight"><pre><span></span><code>agda<span class="o">.</span>withPackages <span class="p">(</span>p<span class="p">:</span> <span class="p">[</span>
|
|
<span class="p">(</span>p<span class="o">.</span>mkDerivation <span class="p">{</span>
|
|
<span class="ss">pname</span> <span class="o">=</span> <span class="s2">"your-agda-lib"</span><span class="p">;</span>
|
|
<span class="ss">version</span> <span class="o">=</span> <span class="s2">"1.0.0"</span><span class="p">;</span>
|
|
<span class="ss">src</span> <span class="o">=</span> fetchFromGitHub <span class="p">{</span>
|
|
<span class="ss">repo</span> <span class="o">=</span> <span class="s2">"repo"</span><span class="p">;</span>
|
|
<span class="ss">owner</span> <span class="o">=</span> <span class="s2">"owner"</span><span class="p">;</span>
|
|
<span class="ss">version</span> <span class="o">=</span> <span class="s2">"..."</span><span class="p">;</span>
|
|
<span class="ss">rev</span> <span class="o">=</span> <span class="s2">"..."</span><span class="p">;</span>
|
|
<span class="ss">hash</span> <span class="o">=</span> <span class="s2">"..."</span><span class="p">;</span>
|
|
<span class="p">};</span>
|
|
<span class="p">})</span>
|
|
<span class="p">])</span>
|
|
</code></pre></div>
|
|
<p>See <a href="#building-agda-packages">Building Agda Packages</a> for more information on <code>mkDerivation</code>.</p>
|
|
<p>Agda will not by default use these libraries. To tell Agda to use a library we have some options:</p>
|
|
<ul>
|
|
<li>Call <code>agda</code> with the library flag:
|
|
<div class="highlight"><pre><span></span><code>$ agda -l standard-library -i . MyFile.agda
|
|
</code></pre></div></li>
|
|
<li>Write a <code>my-library.agda-lib</code> file for the project you are working on which may look like:
|
|
<div class="highlight"><pre><span></span><code>name: my-library
|
|
include: .
|
|
depend: standard-library
|
|
</code></pre></div></li>
|
|
<li>Create the file <code>~/.agda/defaults</code> and add any libraries you want to use by default.</li>
|
|
</ul>
|
|
<p>More information can be found in the <a href="https://agda.readthedocs.io/en/v2.6.1/tools/package-system.html">official Agda documentation on library management</a>.</p>
|
|
<h2 id="compiling-agda">Compiling Agda</h2>
|
|
<p>Agda modules can be compiled using the GHC backend with the <code>--compile</code> flag. A version of <code>ghc</code> with <code>ieee754</code> is made available to the Agda program via the <code>--with-compiler</code> flag.
|
|
This can be overridden by a different version of <code>ghc</code> as follows:</p>
|
|
<div class="highlight"><pre><span></span><code>agda<span class="o">.</span>withPackages <span class="p">{</span>
|
|
<span class="ss">pkgs</span> <span class="o">=</span> <span class="p">[</span> <span class="cm">/* ... */</span> <span class="p">];</span>
|
|
<span class="ss">ghc</span> <span class="o">=</span> haskell<span class="o">.</span>compiler<span class="o">.</span>ghcHEAD<span class="p">;</span>
|
|
<span class="p">}</span>
|
|
</code></pre></div>
|
|
<h2 id="writing-agda-packages">Writing Agda packages</h2>
|
|
<p>To write a nix derivation for an Agda library, first check that the library has a <code>*.agda-lib</code> file.</p>
|
|
<p>A derivation can then be written using <code>agdaPackages.mkDerivation</code>. This has similar arguments to <code>stdenv.mkDerivation</code> with the following additions:</p>
|
|
<ul>
|
|
<li><code>everythingFile</code> can be used to specify the location of the <code>Everything.agda</code> file, defaulting to <code>./Everything.agda</code>. If this file does not exist then either it should be patched in or the <code>buildPhase</code> should be overridden (see below).</li>
|
|
<li><code>libraryName</code> should be the name that appears in the <code>*.agda-lib</code> file, defaulting to <code>pname</code>.</li>
|
|
<li><code>libraryFile</code> should be the file name of the <code>*.agda-lib</code> file, defaulting to <code>${libraryName}.agda-lib</code>.</li>
|
|
</ul>
|
|
<p>Here is an example <code>default.nix</code></p>
|
|
<div class="highlight"><pre><span></span><code><span class="p">{</span> nixpkgs <span class="o">?</span> <span class="l"><nixpkgs></span> <span class="p">}:</span>
|
|
<span class="k">with</span> <span class="p">(</span><span class="nb">import</span> nixpkgs <span class="p">{});</span>
|
|
agdaPackages<span class="o">.</span>mkDerivation <span class="p">{</span>
|
|
<span class="ss">version</span> <span class="o">=</span> <span class="s2">"1.0"</span><span class="p">;</span>
|
|
<span class="ss">pname</span> <span class="o">=</span> <span class="s2">"my-agda-lib"</span><span class="p">;</span>
|
|
<span class="ss">src</span> <span class="o">=</span> <span class="l">./.</span><span class="p">;</span>
|
|
<span class="ss">buildInputs</span> <span class="o">=</span> <span class="p">[</span>
|
|
agdaPackages<span class="o">.</span>standard-library
|
|
<span class="p">];</span>
|
|
<span class="p">}</span>
|
|
</code></pre></div>
|
|
<h3 id="building-agda-packages">Building Agda packages</h3>
|
|
<p>The default build phase for <code>agdaPackages.mkDerivation</code> runs <code>agda</code> on the <code>Everything.agda</code> file.
|
|
If something else is needed to build the package (e.g. <code>make</code>) then the <code>buildPhase</code> should be overridden.
|
|
Additionally, a <code>preBuild</code> or <code>configurePhase</code> can be used if there are steps that need to be done prior to checking the <code>Everything.agda</code> file.
|
|
<code>agda</code> and the Agda libraries contained in <code>buildInputs</code> are made available during the build phase.</p>
|
|
<h3 id="installing-agda-packages">Installing Agda packages</h3>
|
|
<p>The default install phase copies Agda source files, Agda interface files (<code>*.agdai</code>) and <code>*.agda-lib</code> files to the output directory.
|
|
This can be overridden.</p>
|
|
<p>By default, Agda sources are files ending on <code>.agda</code>, or literate Agda files ending on <code>.lagda</code>, <code>.lagda.tex</code>, <code>.lagda.org</code>, <code>.lagda.md</code>, <code>.lagda.rst</code>. The list of recognised Agda source extensions can be extended by setting the <code>extraExtensions</code> config variable.</p>
|
|
<h2 id="maintaining-the-agda-package-set-on-nixpkgs">Maintaining the Agda package set on Nixpkgs</h2>
|
|
<p>We are aiming at providing all common Agda libraries as packages on <code>nixpkgs</code>,
|
|
and keeping them up to date.
|
|
Contributions and maintenance help is always appreciated,
|
|
but the maintenance effort is typically low since the Agda ecosystem is quite small.</p>
|
|
<p>The <code>nixpkgs</code> Agda package set tries to take up a role similar to that of <a href="https://www.stackage.org/">Stackage</a> in the Haskell world.
|
|
It is a curated set of libraries that:</p>
|
|
<ol>
|
|
<li>Always work together.</li>
|
|
<li>Are as up-to-date as possible.</li>
|
|
</ol>
|
|
<p>While the Haskell ecosystem is huge, and Stackage is highly automatised,
|
|
the Agda package set is small and can (still) be maintained by hand.</p>
|
|
<h3 id="adding-agda-packages-to-nixpkgs">Adding Agda packages to Nixpkgs</h3>
|
|
<p>To add an Agda package to <code>nixpkgs</code>, the derivation should be written to <code>pkgs/development/libraries/agda/${library-name}/</code> and an entry should be added to <code>pkgs/top-level/agda-packages.nix</code>. Here it is called in a scope with access to all other Agda libraries, so the top line of the <code>default.nix</code> can look like:</p>
|
|
<div class="highlight"><pre><span></span><code><span class="p">{</span> mkDerivation<span class="p">,</span> standard-library<span class="p">,</span> fetchFromGitHub <span class="p">}:</span>
|
|
<span class="p">{}</span>
|
|
</code></pre></div>
|
|
<p>Note that the derivation function is called with <code>mkDerivation</code> set to <code>agdaPackages.mkDerivation</code>, therefore you
|
|
could use a similar set as in your <code>default.nix</code> from <a href="#writing-agda-packages">Writing Agda Packages</a> with
|
|
<code>agdaPackages.mkDerivation</code> replaced with <code>mkDerivation</code>.</p>
|
|
<p>Here is an example skeleton derivation for iowa-stdlib:</p>
|
|
<div class="highlight"><pre><span></span><code>mkDerivation <span class="p">{</span>
|
|
<span class="ss">version</span> <span class="o">=</span> <span class="s2">"1.5.0"</span><span class="p">;</span>
|
|
<span class="ss">pname</span> <span class="o">=</span> <span class="s2">"iowa-stdlib"</span><span class="p">;</span>
|
|
|
|
<span class="ss">src</span> <span class="o">=</span> <span class="l"><...></span><span class="p">;</span>
|
|
|
|
<span class="ss">libraryFile</span> <span class="o">=</span> <span class="s2">""</span><span class="p">;</span>
|
|
<span class="ss">libraryName</span> <span class="o">=</span> <span class="s2">"IAL-1.3"</span><span class="p">;</span>
|
|
|
|
<span class="ss">buildPhase</span> <span class="o">=</span> <span class="s s-Multiline">''</span>
|
|
<span class="s s-Multiline"> patchShebangs find-deps.sh</span>
|
|
<span class="s s-Multiline"> make</span>
|
|
<span class="s s-Multiline"> ''</span><span class="p">;</span>
|
|
<span class="p">}</span>
|
|
</code></pre></div>
|
|
<p>This library has a file called <code>.agda-lib</code>, and so we give an empty string to <code>libraryFile</code> as nothing precedes <code>.agda-lib</code> in the filename. This file contains <code>name: IAL-1.3</code>, and so we let <code>libraryName = "IAL-1.3"</code>. This library does not use an <code>Everything.agda</code> file and instead has a Makefile, so there is no need to set <code>everythingFile</code> and we set a custom <code>buildPhase</code>.</p>
|
|
<p>When writing an Agda package it is essential to make sure that no <code>.agda-lib</code> file gets added to the store as a single file (for example by using <code>writeText</code>). This causes Agda to think that the nix store is a Agda library and it will attempt to write to it whenever it typechecks something. See <a href="https://github.com/agda/agda/issues/4613">https://github.com/agda/agda/issues/4613</a>.</p>
|
|
<p>In the pull request adding this library,
|
|
you can test whether it builds correctly by writing in a comment:</p>
|
|
<div class="highlight"><pre><span></span><code>@ofborg build agdaPackages.iowa-stdlib
|
|
</code></pre></div>
|
|
<h3 id="agda-maintaining-packages">Maintaining Agda packages</h3>
|
|
<p>As mentioned before, the aim is to have a compatible, and up-to-date package set.
|
|
These two conditions sometimes exclude each other:
|
|
For example, if we update <code>agdaPackages.standard-library</code> because there was an upstream release,
|
|
this will typically break many reverse dependencies,
|
|
i.e. downstream Agda libraries that depend on the standard library.
|
|
In <code>nixpkgs</code> we are typically among the first to notice this,
|
|
since we have build tests in place to check this.</p>
|
|
<p>In a pull request updating e.g. the standard library, you should write the following comment:</p>
|
|
<div class="highlight"><pre><span></span><code>@ofborg build agdaPackages.standard-library.passthru.tests
|
|
</code></pre></div>
|
|
<p>This will build all reverse dependencies of the standard library,
|
|
for example <code>agdaPackages.agda-categories</code>, or <code>agdaPackages.generic</code>.</p>
|
|
<p>In some cases it is useful to build <em>all</em> Agda packages.
|
|
This can be done with the following Github comment:</p>
|
|
<div class="highlight"><pre><span></span><code>@ofborg build agda.passthru.tests.allPackages
|
|
</code></pre></div>
|
|
<p>Sometimes, the builds of the reverse dependencies fail because they have not yet been updated and released.
|
|
You should drop the maintainers a quick issue notifying them of the breakage,
|
|
citing the build error (which you can get from the ofborg logs).
|
|
If you are motivated, you might even send a pull request that fixes it.
|
|
Usually, the maintainers will answer within a week or two with a new release.
|
|
Bumping the version of that reverse dependency should be a further commit on your PR.</p>
|
|
<p>In the rare case that a new release is not to be expected within an acceptable time,
|
|
mark the broken package as broken by setting <code>meta.broken = true;</code>.
|
|
This will exclude it from the build test.
|
|
It can be added later when it is fixed,
|
|
and does not hinder the advancement of the whole package set in the meantime.</p>
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
</article>
|
|
</div>
|
|
|
|
|
|
<script>var target=document.getElementById(location.hash.slice(1));target&&target.name&&(target.checked=target.name.startsWith("__tabbed_"))</script>
|
|
</div>
|
|
|
|
</main>
|
|
|
|
<footer class="md-footer">
|
|
|
|
<div class="md-footer-meta md-typeset">
|
|
<div class="md-footer-meta__inner md-grid">
|
|
<div class="md-copyright">
|
|
|
|
<div class="md-copyright__highlight">
|
|
Licenced MIT
|
|
</div>
|
|
|
|
|
|
Made with
|
|
<a href="https://squidfunk.github.io/mkdocs-material/" target="_blank" rel="noopener">
|
|
Material for MkDocs
|
|
</a>
|
|
|
|
</div>
|
|
|
|
<div class="md-social">
|
|
|
|
|
|
|
|
|
|
|
|
<a href="https://git.auxolotl.org/auxolotl/docs" target="_blank" rel="noopener" title="Aux Docs Repo" class="md-social__link">
|
|
<svg xmlns="http://www.w3.org/2000/svg" viewBox="0 0 24 24"><path d="M16.777 0a2.9 2.9 0 1 1-2.529 4.322H12.91a4.266 4.266 0 0 0-4.265 4.195v2.118a7.076 7.076 0 0 1 4.147-1.42l.118-.002h1.338a2.9 2.9 0 0 1 5.43 1.422 2.9 2.9 0 0 1-5.43 1.422H12.91a4.266 4.266 0 0 0-4.265 4.195v2.319A2.9 2.9 0 0 1 7.222 24 2.9 2.9 0 0 1 5.8 18.57V8.589a7.109 7.109 0 0 1 6.991-7.108l.118-.001h1.338A2.9 2.9 0 0 1 16.778 0ZM7.223 19.905a1.194 1.194 0 1 0 0 2.389 1.194 1.194 0 0 0 0-2.389Zm9.554-10.464a1.194 1.194 0 1 0 0 2.389 1.194 1.194 0 0 0 0-2.39Zm0-7.735a1.194 1.194 0 1 0 0 2.389 1.194 1.194 0 0 0 0-2.389Z"/></svg>
|
|
</a>
|
|
|
|
|
|
|
|
|
|
|
|
<a href="https://forum.aux.computer/" target="_blank" rel="noopener" title="Aux Forum" class="md-social__link">
|
|
<svg xmlns="http://www.w3.org/2000/svg" viewBox="0 0 24 24"><path d="M12.103 0C18.666 0 24 5.485 24 11.997c0 6.51-5.33 11.99-11.9 11.99L0 24V11.79C0 5.28 5.532 0 12.103 0zm.116 4.563a7.395 7.395 0 0 0-6.337 3.57 7.247 7.247 0 0 0-.148 7.22L4.4 19.61l4.794-1.074a7.424 7.424 0 0 0 8.136-1.39 7.256 7.256 0 0 0 1.737-7.997 7.375 7.375 0 0 0-6.84-4.585h-.008z"/></svg>
|
|
</a>
|
|
|
|
|
|
|
|
|
|
|
|
<a href="https://wiki.auxolotl.org/" target="_blank" rel="noopener" title="Aux Wiki" class="md-social__link">
|
|
<svg xmlns="http://www.w3.org/2000/svg" viewBox="0 0 24 24"><path d="M17.801 13.557c.148.098.288.202.417.313 1.854 1.6 3.127 4.656 2.582 7.311-1.091-.255-5.747-1.055-7.638-3.383-.91-1.12-1.366-2.081-1.569-2.885a5.65 5.65 0 0 0 .034-.219c.089.198.197.35.313.466.24.24.521.335.766.372.304.046.594-.006.806-.068l.001.001c.05-.015.433-.116.86-.342.325-.173 2.008-.931 3.428-1.566Zm-7.384 1.435C9.156 16.597 6.6 18.939.614 18.417c.219-1.492 1.31-3.019 2.51-4.11.379-.345.906-.692 1.506-1.009.286.168.598.332.939.486 2.689 1.221 3.903 1.001 4.89.573a1.3 1.3 0 0 0 .054-.025 6.156 6.156 0 0 0-.096.66Zm4.152-.462c.38-.341.877-.916 1.383-1.559-.389-.15-.866-.371-1.319-.591-.598-.29-1.305-.283-2.073-.315a4.685 4.685 0 0 1-.804-.103c.014-.123.027-.246.038-.369.062.104.673.057.871.057.354 0 1.621.034 3.074-.574 1.452-.608 2.55-1.706 3.022-3.225.474-1.52.22-3.091-.168-3.952-.169.709-1.453 2.381-1.926 2.871-.473.489-2.381 2.296-2.972 2.921-.7.74-.688.793-1.332 1.302-.202.19-.499.402-.563.53.027-.338.039-.675.027-.997a7.653 7.653 0 0 0-.032-.523c.322-.059.567-.522.567-.861 0-.224-.106-.247-.271-.229.075-.894.382-3.923 1.254-4.281.218.109.831.068.649-.295-.182-.364-.825-.074-1.081.266-.28.374-.956 2.046-.92 4.324-.113.014-.174.033-.322.033-.171 0-.321-.04-.433-.05.034-2.275-.714-3.772-.84-4.169-.12-.375-.491-.596-.781-.596-.146 0-.272.056-.333.179-.182.363.459.417.677.308.706.321 1.156 3.519 1.254 4.277-.125-.006-.199.035-.199.233 0 .311.17.756.452.843a.442.442 0 0 0-.007.03s-.287.99-.413 2.189a4.665 4.665 0 0 1-.718-.225c-.714-.286-1.355-.583-2.019-.566-.664.018-1.366.023-1.804-.036-.438-.058-.649-.15-.649-.15s-.234.365.257 1.075c.42.607 1.055 1.047 1.644 1.18.589.134 1.972.18 2.785-.377.16-.109.317-.228.459-.34a8.717 8.717 0 0 0-.013.626c-.289.753-.571 1.993-.268 3.338 0-.001.701-.842.787-2.958.006-.144.009-.271.01-.383.052-.248.103-.518.148-.799.072.135.151.277.234.413.511.842 1.791 1.37 2.383 1.49.091.019.187.032.285.038Zm-1.12.745c-.188.055-.445.1-.713.059-.21-.031-.45-.11-.655-.316-.169-.168-.312-.419-.401-.789a9.837 9.837 0 0 0 .039-.82l.049-.243c.563.855 1.865 1.398 2.476 1.522.036.008.072.014.109.02l-.013.009c-.579.415-.76.503-.891.558Zm6.333-2.818c-.257.114-4.111 1.822-5.246 2.363.98-.775 3.017-3.59 3.699-4.774 1.062.661 1.468 1.109 1.623 1.441.101.217.09.38.096.515a.57.57 0 0 1-.172.455Zm-9.213 1.62a1.606 1.606 0 0 1-.19.096c-.954.414-2.126.61-4.728-.571-2.023-.918-3.024-2.157-3.371-2.666.476.161 1.471.473 2.157.524.282.021.703.068 1.167.125.021.209.109.486.345.829l.001.001c.451.651 1.134 1.119 1.765 1.262.622.141 2.083.182 2.942-.407a3.12 3.12 0 0 0 .132-.093l.001.179a6.052 6.052 0 0 0-.221.721Zm5.512-1.271a17.49 17.49 0 0 1-1.326-.589c.437.042 1.054.083 1.692.108-.121.162-.244.323-.366.481Zm.932-1.26c-.12.17-.245.343-.373.517-.241.018-.478.03-.709.038a29.05 29.05 0 0 1-.741-.048c.608-.065 1.228-.252 1.823-.507Zm.22-.315c-.809.382-1.679.648-2.507.648-.472 0-.833.018-1.139.039v.001c-.324-.031-.665-.039-1.019-.054a3.555 3.555 0 0 1-.152-.009c.102-.002.192-.006.249-.006.363 0 1.662.034 3.151-.589 1.508-.632 2.645-1.773 3.136-3.351.37-1.186.31-2.402.086-3.312.458-.336.86-.651 1.147-.91.501-.451.743-.733.848-.869.199.206.714.864.685 2.138-.036 1.611-.606 3.187-1.501 4.154a9.099 9.099 0 0 1-1.321 1.132 11.978 11.978 0 0 0-.644-.422l-.089-.055-.051.091c-.184.332-.5.825-.879 1.374ZM4.763 5.817c-.157 1.144.113 2.323.652 3.099.539.776 2.088 2.29 3.614 2.505.991.14 2.055.134 2.055.134s-.593-.576-1.114-1.66c-.521-1.085-.948-2.104-1.734-2.786-.785-.681-1.601-1.416-2.045-1.945-.444-.53-.59-.86-.59-.86s-.656.175-.838 1.513Zm14.301 4.549a9.162 9.162 0 0 0 1.3-1.12c.326-.352.611-.782.845-1.265 1.315.145 2.399.371 2.791.434 0 0-.679 1.971-3.945 3.022l-.016-.035c-.121-.26-.385-.594-.975-1.036Zm-11.634.859a8.537 8.537 0 0 1-.598-.224c-1.657-.693-2.91-1.944-3.449-3.678-.498-1.601-.292-3.251.091-4.269.225.544.758 1.34 1.262 2.01a3.58 3.58 0 0 0-.172.726c-.163 1.197.123 2.428.687 3.24.416.599 1.417 1.62 2.555 2.193-.128.002-.253.003-.376.002Zm-1.758-.077c-.958-.341-1.901-.787-2.697-1.368C-.07 7.559 0 6.827 0 6.827s1.558-.005 3.088.179c.03.126.065.251.104.377.557 1.791 1.851 3.086 3.562 3.803l.047.019a4.254 4.254 0 0 1-.267-.026h-.001c-.401-.053-.595-.135-.595-.135l-.157-.069-.092.144-.017.029Zm6.807-1.59c.086.017.136.058.136.145 0 .197-.242.5-.597.597l-.01-.161a.887.887 0 0 0 .283-.243c.078-.099.142-.217.188-.338Zm-1.591.006c.033.1.076.197.129.282.061.097.134.18.217.24l-.021.083c-.276-.093-.424-.293-.424-.466 0-.078.035-.119.099-.139Zm-.025-.664c-.275-.816-.795-2.022-1.505-2.179-.296.072-.938.096-.691-.145.246-.24 1.085-.048 1.283.217.145.194.744.806 1.011 1.737l.032.227a.324.324 0 0 0-.13.143Zm1.454-.266c.251-.99.889-1.639 1.039-1.841.197-.265 1.036-.457 1.283-.217.247.241-.395.217-.691.145-.69.152-1.2 1.296-1.481 2.109a.364.364 0 0 0-.067-.059.37.37 0 0 0-.092-.043l.009-.094Zm4.802-2.708a9.875 9.875 0 0 1-.596.705c-.304.315-1.203 1.176-1.963 1.916.647-.955 1.303-1.806 2.184-2.376.123-.08.249-.161.375-.245Z"/></svg>
|
|
</a>
|
|
|
|
</div>
|
|
|
|
</div>
|
|
</div>
|
|
</footer>
|
|
|
|
</div>
|
|
<div class="md-dialog" data-md-component="dialog">
|
|
<div class="md-dialog__inner md-typeset"></div>
|
|
</div>
|
|
|
|
|
|
<script id="__config" type="application/json">{"base": "../../..", "features": ["content.tooltips", "search.highlight", "navigation.tabs", "navigation.indexes", "navigation.prune"], "search": "../../../assets/javascripts/workers/search.b8dbb3d2.min.js", "translations": {"clipboard.copied": "Copied to clipboard", "clipboard.copy": "Copy to clipboard", "search.result.more.one": "1 more on this page", "search.result.more.other": "# more on this page", "search.result.none": "No matching documents", "search.result.one": "1 matching document", "search.result.other": "# matching documents", "search.result.placeholder": "Type to start searching", "search.result.term.missing": "Missing", "select.version": "Select version"}}</script>
|
|
|
|
|
|
<script src="../../../assets/javascripts/bundle.fe8b6f2b.min.js"></script>
|
|
|
|
|
|
</body>
|
|
</html> |