minion/docs
1
0
Fork 0
forked from auxolotl/docs
Code Pull requests 5 Activity
docs/Nixpkgs/Languages-And-Frameworks/agda.section/index.html

3061 lines
66 KiB
HTML
Raw Permalink Normal View History

Deploy cd4936a to pages...pages.gay
2024-07-24 19:14:02 +00:00
<!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 &amp; 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&amp;show=agda&amp;from=0&amp;size=30&amp;sort=relevance&amp;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">&quot;local version&quot;</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">&quot;1.5&quot;</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">&quot;agda-stdlib&quot;</span><span class="p">;</span>
<span class="ss">owner</span> <span class="o">=</span> <span class="s2">&quot;agda&quot;</span><span class="p">;</span>
<span class="ss">rev</span> <span class="o">=</span> <span class="s2">&quot;v1.5&quot;</span><span class="p">;</span>
<span class="ss">hash</span> <span class="o">=</span> <span class="s2">&quot;sha256-nEyxYGSWIDNJqBfGpRDLiOAnlHJKEKAOMnIaqfVZzJk=&quot;</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">&quot;your-agda-lib&quot;</span><span class="p">;</span>
<span class="ss">version</span> <span class="o">=</span> <span class="s2">&quot;1.0.0&quot;</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">&quot;your-agda-lib&quot;</span><span class="p">;</span>
<span class="ss">version</span> <span class="o">=</span> <span class="s2">&quot;1.0.0&quot;</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">&quot;repo&quot;</span><span class="p">;</span>
<span class="ss">owner</span> <span class="o">=</span> <span class="s2">&quot;owner&quot;</span><span class="p">;</span>
<span class="ss">version</span> <span class="o">=</span> <span class="s2">&quot;...&quot;</span><span class="p">;</span>
<span class="ss">rev</span> <span class="o">=</span> <span class="s2">&quot;...&quot;</span><span class="p">;</span>
<span class="ss">hash</span> <span class="o">=</span> <span class="s2">&quot;...&quot;</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">&lt;nixpkgs&gt;</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">&quot;1.0&quot;</span><span class="p">;</span>
<span class="ss">pname</span> <span class="o">=</span> <span class="s2">&quot;my-agda-lib&quot;</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">&quot;1.5.0&quot;</span><span class="p">;</span>
<span class="ss">pname</span> <span class="o">=</span> <span class="s2">&quot;iowa-stdlib&quot;</span><span class="p">;</span>
<span class="ss">src</span> <span class="o">=</span> <span class="l">&lt;...&gt;</span><span class="p">;</span>
<span class="ss">libraryFile</span> <span class="o">=</span> <span class="s2">&quot;&quot;</span><span class="p">;</span>
<span class="ss">libraryName</span> <span class="o">=</span> <span class="s2">&quot;IAL-1.3&quot;</span><span class="p">;</span>
<span class="ss">buildPhase</span> <span class="o">=</span> <span class="s s-Multiline">&#39;&#39;</span>
<span class="s s-Multiline"> patchShebangs find-deps.sh</span>
<span class="s s-Multiline"> make</span>
<span class="s s-Multiline"> &#39;&#39;</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.
</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>
Copy permalink