auxolotl/docs
26
0
Fork 1
mirror of https://git.gay/pyrox/aux-docs synced 2024-11-23 10:47:58 +00:00
Code Issues Packages Projects Releases Wiki Activity
docs/Nixpkgs/Languages-And-Frameworks/coq.section/index.html

2940 lines
70 KiB
HTML
Raw Permalink Blame History

<!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/coq.section/">
<link rel="prev" href="../chicken.section/">
<link rel="next" href="../crystal.section/">
<link rel="icon" href="../../../assets/aux-logo.svg">
<meta name="generator" content="mkdocs-1.6.0, mkdocs-material-9.5.29">
<title>Coq and coq packages - 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="Coq and coq packages {#sec-language-coq} - 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/coq.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/coq.section/" >
<meta name="twitter:card" content="summary_large_image" >
<meta name="twitter:title" content="Coq and coq packages {#sec-language-coq} - 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/coq.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="#sec-language-coq" 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">
Coq and coq packages
</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">
<a href="../agda.section/" class="md-nav__link">
<span class="md-ellipsis">
Agda
</span>
</a>
</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 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">
Coq and coq packages
</span>
<span class="md-nav__icon md-icon"></span>
</label>
<a href="./" class="md-nav__link md-nav__link--active">
<span class="md-ellipsis">
Coq and coq packages
</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="#coq-derivation-coq" class="md-nav__link">
<span class="md-ellipsis">
Coq derivation: coq
</span>
</a>
</li>
<li class="md-nav__item">
<a href="#coq-packages-attribute-sets-coqpackages" class="md-nav__link">
<span class="md-ellipsis">
Coq packages attribute sets: coqPackages
</span>
</a>
</li>
<li class="md-nav__item">
<a href="#coq-overriding-packages" class="md-nav__link">
<span class="md-ellipsis">
Three ways of overriding Coq packages
</span>
</a>
<nav class="md-nav" aria-label="Three ways of overriding Coq packages">
<ul class="md-nav__list">
<li class="md-nav__item">
<a href="#coq-override" class="md-nav__link">
<span class="md-ellipsis">
.override
</span>
</a>
</li>
<li class="md-nav__item">
<a href="#coq-overrideCoqDerivation" class="md-nav__link">
<span class="md-ellipsis">
overrideCoqDerivation
</span>
</a>
</li>
<li class="md-nav__item">
<a href="#coq-overrideAttrs" class="md-nav__link">
<span class="md-ellipsis">
.overrideAttrs
</span>
</a>
</li>
</ul>
</nav>
</li>
</ul>
</nav>
</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="#coq-derivation-coq" class="md-nav__link">
<span class="md-ellipsis">
Coq derivation: coq
</span>
</a>
</li>
<li class="md-nav__item">
<a href="#coq-packages-attribute-sets-coqpackages" class="md-nav__link">
<span class="md-ellipsis">
Coq packages attribute sets: coqPackages
</span>
</a>
</li>
<li class="md-nav__item">
<a href="#coq-overriding-packages" class="md-nav__link">
<span class="md-ellipsis">
Three ways of overriding Coq packages
</span>
</a>
<nav class="md-nav" aria-label="Three ways of overriding Coq packages">
<ul class="md-nav__list">
<li class="md-nav__item">
<a href="#coq-override" class="md-nav__link">
<span class="md-ellipsis">
.override
</span>
</a>
</li>
<li class="md-nav__item">
<a href="#coq-overrideCoqDerivation" class="md-nav__link">
<span class="md-ellipsis">
overrideCoqDerivation
</span>
</a>
</li>
<li class="md-nav__item">
<a href="#coq-overrideAttrs" class="md-nav__link">
<span class="md-ellipsis">
.overrideAttrs
</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="sec-language-coq">Coq and coq packages</h1>
<h2 id="coq-derivation-coq">Coq derivation: <code>coq</code></h2>
<p>The Coq derivation is overridable through the <code>coq.override overrides</code>, where overrides is an attribute set which contains the arguments to override. We recommend overriding either of the following</p>
<ul>
<li><code>version</code> (optional, defaults to the latest version of Coq selected for nixpkgs, see <code>pkgs/top-level/coq-packages</code> to witness this choice), which follows the conventions explained in the <code>coqPackages</code> section below,</li>
<li><code>customOCamlPackages</code> (optional, defaults to <code>null</code>, which lets Coq choose a version automatically), which can be set to any of the ocaml packages attribute of <code>ocaml-ng</code> (such as <code>ocaml-ng.ocamlPackages_4_10</code> which is the default for Coq 8.11 for example).</li>
<li><code>coq-version</code> (optional, defaults to the short version e.g. "8.10"), is a version number of the form "x.y" that indicates which Coq's version build behavior to mimic when using a source which is not a release. E.g. <code>coq.override { version = "d370a9d1328a4e1cdb9d02ee032f605a9d94ec7a"; coq-version = "8.10"; }</code>.</li>
</ul>
<p>The associated package set can be obtained using <code>mkCoqPackages coq</code>, where <code>coq</code> is the derivation to use.</p>
<h2 id="coq-packages-attribute-sets-coqpackages">Coq packages attribute sets: <code>coqPackages</code></h2>
<p>The recommended way of defining a derivation for a Coq library, is to use the <code>coqPackages.mkCoqDerivation</code> function, which is essentially a specialization of <code>mkDerivation</code> taking into account most of the specifics of Coq libraries. The following attributes are supported:</p>
<ul>
<li><code>pname</code> (required) is the name of the package,</li>
<li><code>version</code> (optional, defaults to <code>null</code>), is the version to fetch and build,
this attribute is interpreted in several ways depending on its type and pattern:</li>
<li>if it is a known released version string, i.e. from the <code>release</code> attribute below, the according release is picked, and the <code>version</code> attribute of the resulting derivation is set to this release string,</li>
<li>if it is a majorMinor <code>"x.y"</code> prefix of a known released version (as defined above), then the latest <code>"x.y.z"</code> known released version is selected (for the ordering given by <code>versionAtLeast</code>),</li>
<li>if it is a path or a string representing an absolute path (i.e. starting with <code>"/"</code>), the provided path is selected as a source, and the <code>version</code> attribute of the resulting derivation is set to <code>"dev"</code>,</li>
<li>if it is a string of the form <code>owner:branch</code> then it tries to download the <code>branch</code> of owner <code>owner</code> for a project of the same name using the same vcs, and the <code>version</code> attribute of the resulting derivation is set to <code>"dev"</code>, additionally if the owner is not provided (i.e. if the <code>owner:</code> prefix is missing), it defaults to the original owner of the package (see below),</li>
<li>if it is a string of the form <code>"#N"</code>, and the domain is github, then it tries to download the current head of the pull request <code>#N</code> from github,</li>
<li><code>defaultVersion</code> (optional). Coq libraries may be compatible with some specific versions of Coq only. The <code>defaultVersion</code> attribute is used when no <code>version</code> is provided (or if <code>version = null</code>) to select the version of the library to use by default, depending on the context. This selection will mainly depend on a <code>coq</code> version number but also possibly on other packages versions (e.g. <code>mathcomp</code>). If its value ends up to be <code>null</code>, the package is marked for removal in end-user <code>coqPackages</code> attribute set.</li>
<li><code>release</code> (optional, defaults to <code>{}</code>), lists all the known releases of the library and for each of them provides an attribute set with at least a <code>sha256</code> attribute (you may put the empty string <code>""</code> in order to automatically insert a fake sha256, this will trigger an error which will allow you to find the correct sha256), each attribute set of the list of releases also takes optional overloading arguments for the fetcher as below (i.e.<code>domain</code>, <code>owner</code>, <code>repo</code>, <code>rev</code> assuming the default fetcher is used) and optional overrides for the result of the fetcher (i.e. <code>version</code> and <code>src</code>).</li>
<li><code>fetcher</code> (optional, defaults to a generic fetching mechanism supporting github or gitlab based infrastructures), is a function that takes at least an <code>owner</code>, a <code>repo</code>, a <code>rev</code>, and a <code>hash</code> and returns an attribute set with a <code>version</code> and <code>src</code>.</li>
<li><code>repo</code> (optional, defaults to the value of <code>pname</code>),</li>
<li><code>owner</code> (optional, defaults to <code>"coq-community"</code>).</li>
<li><code>domain</code> (optional, defaults to <code>"github.com"</code>), domains including the strings <code>"github"</code> or <code>"gitlab"</code> in their names are automatically supported, otherwise, one must change the <code>fetcher</code> argument to support them (cf <code>pkgs/development/coq-modules/heq/default.nix</code> for an example),</li>
<li><code>releaseRev</code> (optional, defaults to <code>(v: v)</code>), provides a default mapping from release names to revision hashes/branch names/tags,</li>
<li><code>displayVersion</code> (optional), provides a way to alter the computation of <code>name</code> from <code>pname</code>, by explaining how to display version numbers,</li>
<li><code>namePrefix</code> (optional, defaults to <code>[ "coq" ]</code>), provides a way to alter the computation of <code>name</code> from <code>pname</code>, by explaining which dependencies must occur in <code>name</code>,</li>
<li><code>nativeBuildInputs</code> (optional), is a list of executables that are required to build the current derivation, in addition to the default ones (namely <code>which</code>, <code>dune</code> and <code>ocaml</code> depending on whether <code>useDune</code>, <code>useDuneifVersion</code> and <code>mlPlugin</code> are set).</li>
<li><code>extraNativeBuildInputs</code> (optional, deprecated), an additional list of derivation to add to <code>nativeBuildInputs</code>,</li>
<li><code>overrideNativeBuildInputs</code> (optional) replaces the default list of derivation to which <code>nativeBuildInputs</code> and <code>extraNativeBuildInputs</code> adds extra elements,</li>
<li><code>buildInputs</code> (optional), is a list of libraries and dependencies that are required to build and run the current derivation, in addition to the default one <code>[ coq ]</code>,</li>
<li><code>extraBuildInputs</code> (optional, deprecated), an additional list of derivation to add to <code>buildInputs</code>,</li>
<li><code>overrideBuildInputs</code> (optional) replaces the default list of derivation to which <code>buildInputs</code> and <code>extraBuildInputs</code> adds extras elements,</li>
<li><code>propagatedBuildInputs</code> (optional) is passed as is to <code>mkDerivation</code>, we recommend to use this for Coq libraries and Coq plugin dependencies, as this makes sure the paths of the compiled libraries and plugins will always be added to the build environments of subsequent derivation, which is necessary for Coq packages to work correctly,</li>
<li><code>mlPlugin</code> (optional, defaults to <code>false</code>). Some extensions (plugins) might require OCaml and sometimes other OCaml packages. Standard dependencies can be added by setting the current option to <code>true</code>. For a finer grain control, the <code>coq.ocamlPackages</code> attribute can be used in <code>nativeBuildInputs</code>, <code>buildInputs</code>, and <code>propagatedBuildInputs</code> to depend on the same package set Coq was built against.</li>
<li><code>useDuneifVersion</code> (optional, default to <code>(x: false)</code> uses Dune to build the package if the provided predicate evaluates to true on the version, e.g. <code>useDuneifVersion = versions.isGe "1.1"</code> will use dune if the version of the package is greater or equal to <code>"1.1"</code>,</li>
<li><code>useDune</code> (optional, defaults to <code>false</code>) uses Dune to build the package if set to true, the presence of this attribute overrides the behavior of the previous one.</li>
<li><code>opam-name</code> (optional, defaults to concatenating with a dash separator the components of <code>namePrefix</code> and <code>pname</code>), name of the Dune package to build.</li>
<li><code>enableParallelBuilding</code> (optional, defaults to <code>true</code>), since it is activated by default, we provide a way to disable it.</li>
<li><code>extraInstallFlags</code> (optional), allows to extend <code>installFlags</code> which initializes the variable <code>COQMF_COQLIB</code> so as to install in the proper subdirectory. Indeed Coq libraries should be installed in <code>$(out)/lib/coq/${coq.coq-version}/user-contrib/</code>. Such directories are automatically added to the <code>$COQPATH</code> environment variable by the hook defined in the Coq derivation.</li>
<li><code>setCOQBIN</code> (optional, defaults to <code>true</code>), by default, the environment variable <code>$COQBIN</code> is set to the current Coq's binary, but one can disable this behavior by setting it to <code>false</code>,</li>
<li><code>useMelquiondRemake</code> (optional, default to <code>null</code>) is an attribute set, which, if given, overloads the <code>preConfigurePhases</code>, <code>configureFlags</code>, <code>buildPhase</code>, and <code>installPhase</code> attributes of the derivation for a specific use in libraries using <code>remake</code> as set up by Guillaume Melquiond for <code>flocq</code>, <code>gappalib</code>, <code>interval</code>, and <code>coquelicot</code> (see the corresponding derivation for concrete examples of use of this option). For backward compatibility, the attribute <code>useMelquiondRemake.logpath</code> must be set to the logical root of the library (otherwise, one can pass <code>useMelquiondRemake = {}</code> to activate this without backward compatibility).</li>
<li><code>dropAttrs</code>, <code>keepAttrs</code>, <code>dropDerivationAttrs</code> are all optional and allow to tune which attribute is added or removed from the final call to <code>mkDerivation</code>.</li>
</ul>
<p>It also takes other standard <code>mkDerivation</code> attributes, they are added as such, except for <code>meta</code> which extends an automatically computed <code>meta</code> (where the <code>platform</code> is the same as <code>coq</code> and the homepage is automatically computed).</p>
<p>Here is a simple package example. It is a pure Coq library, thus it depends on Coq. It builds on the Mathematical Components library, thus it also takes some <code>mathcomp</code> derivations as <code>extraBuildInputs</code>.</p>
<div class="highlight"><pre><span></span><code><span class="p">{</span> lib<span class="p">,</span> mkCoqDerivation<span class="p">,</span> version <span class="o">?</span> <span class="no">null</span>
<span class="p">,</span> coq<span class="p">,</span> mathcomp<span class="p">,</span> mathcomp-finmap<span class="p">,</span> mathcomp-bigenough <span class="p">}:</span>
mkCoqDerivation <span class="p">{</span>
<span class="cm">/* namePrefix leads to e.g. `name = coq8.11-mathcomp1.11-multinomials-1.5.2` */</span>
<span class="ss">namePrefix</span> <span class="o">=</span> <span class="p">[</span> <span class="s2">&quot;coq&quot;</span> <span class="s2">&quot;mathcomp&quot;</span> <span class="p">];</span>
<span class="ss">pname</span> <span class="o">=</span> <span class="s2">&quot;multinomials&quot;</span><span class="p">;</span>
<span class="ss">owner</span> <span class="o">=</span> <span class="s2">&quot;math-comp&quot;</span><span class="p">;</span>
<span class="k">inherit</span> version<span class="p">;</span>
<span class="ss">defaultVersion</span> <span class="o">=</span> <span class="k">with</span> lib<span class="o">.</span>versions<span class="p">;</span> lib<span class="o">.</span>switch <span class="p">[</span> coq<span class="o">.</span>version mathcomp<span class="o">.</span>version <span class="p">]</span> <span class="p">[</span>
<span class="p">{</span> <span class="ss">cases</span> <span class="o">=</span> <span class="p">[</span> <span class="p">(</span>range <span class="s2">&quot;8.7&quot;</span> <span class="s2">&quot;8.12&quot;</span><span class="p">)</span> <span class="p">(</span>isEq <span class="s2">&quot;1.11&quot;</span><span class="p">)</span> <span class="p">];</span> <span class="ss">out</span> <span class="o">=</span> <span class="s2">&quot;1.5.2&quot;</span><span class="p">;</span> <span class="p">}</span>
<span class="p">{</span> <span class="ss">cases</span> <span class="o">=</span> <span class="p">[</span> <span class="p">(</span>range <span class="s2">&quot;8.7&quot;</span> <span class="s2">&quot;8.11&quot;</span><span class="p">)</span> <span class="p">(</span>range <span class="s2">&quot;1.8&quot;</span> <span class="s2">&quot;1.10&quot;</span><span class="p">)</span> <span class="p">];</span> <span class="ss">out</span> <span class="o">=</span> <span class="s2">&quot;1.5.0&quot;</span><span class="p">;</span> <span class="p">}</span>
<span class="p">{</span> <span class="ss">cases</span> <span class="o">=</span> <span class="p">[</span> <span class="p">(</span>range <span class="s2">&quot;8.7&quot;</span> <span class="s2">&quot;8.10&quot;</span><span class="p">)</span> <span class="p">(</span>range <span class="s2">&quot;1.8&quot;</span> <span class="s2">&quot;1.10&quot;</span><span class="p">)</span> <span class="p">];</span> <span class="ss">out</span> <span class="o">=</span> <span class="s2">&quot;1.4&quot;</span><span class="p">;</span> <span class="p">}</span>
<span class="p">{</span> <span class="ss">cases</span> <span class="o">=</span> <span class="p">[</span> <span class="p">(</span>isEq <span class="s2">&quot;8.6&quot;</span><span class="p">)</span> <span class="p">(</span>range <span class="s2">&quot;1.6&quot;</span> <span class="s2">&quot;1.7&quot;</span><span class="p">)</span> <span class="p">];</span> <span class="ss">out</span> <span class="o">=</span> <span class="s2">&quot;1.1&quot;</span><span class="p">;</span> <span class="p">}</span>
<span class="p">]</span> <span class="no">null</span><span class="p">;</span>
<span class="ss">release</span> <span class="o">=</span> <span class="p">{</span>
<span class="s2">&quot;1.5.2&quot;</span><span class="o">.</span><span class="ss">sha256</span> <span class="o">=</span> <span class="s2">&quot;15aspf3jfykp1xgsxf8knqkxv8aav2p39c2fyirw7pwsfbsv2c4s&quot;</span><span class="p">;</span>
<span class="s2">&quot;1.5.1&quot;</span><span class="o">.</span><span class="ss">sha256</span> <span class="o">=</span> <span class="s2">&quot;13nlfm2wqripaq671gakz5mn4r0xwm0646araxv0nh455p9ndjs3&quot;</span><span class="p">;</span>
<span class="s2">&quot;1.5.0&quot;</span><span class="o">.</span><span class="ss">sha256</span> <span class="o">=</span> <span class="s2">&quot;064rvc0x5g7y1a0nip6ic91vzmq52alf6in2bc2dmss6dmzv90hw&quot;</span><span class="p">;</span>
<span class="s2">&quot;1.5.0&quot;</span><span class="o">.</span><span class="ss">rev</span> <span class="o">=</span> <span class="s2">&quot;1.5&quot;</span><span class="p">;</span>
<span class="s2">&quot;1.4&quot;</span><span class="o">.</span><span class="ss">sha256</span> <span class="o">=</span> <span class="s2">&quot;0vnkirs8iqsv8s59yx1fvg1nkwnzydl42z3scya1xp1b48qkgn0p&quot;</span><span class="p">;</span>
<span class="s2">&quot;1.3&quot;</span><span class="o">.</span><span class="ss">sha256</span> <span class="o">=</span> <span class="s2">&quot;0l3vi5n094nx3qmy66hsv867fnqm196r8v605kpk24gl0aa57wh4&quot;</span><span class="p">;</span>
<span class="s2">&quot;1.2&quot;</span><span class="o">.</span><span class="ss">sha256</span> <span class="o">=</span> <span class="s2">&quot;1mh1w339dslgv4f810xr1b8v2w7rpx6fgk9pz96q0fyq49fw2xcq&quot;</span><span class="p">;</span>
<span class="s2">&quot;1.1&quot;</span><span class="o">.</span><span class="ss">sha256</span> <span class="o">=</span> <span class="s2">&quot;1q8alsm89wkc0lhcvxlyn0pd8rbl2nnxg81zyrabpz610qqjqc3s&quot;</span><span class="p">;</span>
<span class="s2">&quot;1.0&quot;</span><span class="o">.</span><span class="ss">sha256</span> <span class="o">=</span> <span class="s2">&quot;1qmbxp1h81cy3imh627pznmng0kvv37k4hrwi2faa101s6bcx55m&quot;</span><span class="p">;</span>
<span class="p">};</span>
<span class="ss">propagatedBuildInputs</span> <span class="o">=</span>
<span class="p">[</span> mathcomp<span class="o">.</span>ssreflect mathcomp<span class="o">.</span>algebra mathcomp-finmap mathcomp-bigenough <span class="p">];</span>
<span class="ss">meta</span> <span class="o">=</span> <span class="p">{</span>
<span class="ss">description</span> <span class="o">=</span> <span class="s2">&quot;Coq/SSReflect Library for Monoidal Rings and Multinomials&quot;</span><span class="p">;</span>
<span class="ss">license</span> <span class="o">=</span> lib<span class="o">.</span>licenses<span class="o">.</span>cecill-c<span class="p">;</span>
<span class="p">};</span>
<span class="p">}</span>
</code></pre></div>
<h2 id="coq-overriding-packages">Three ways of overriding Coq packages</h2>
<p>There are three distinct ways of changing a Coq package by overriding one of its values: <code>.override</code>, <code>overrideCoqDerivation</code>, and <code>.overrideAttrs</code>. This section explains what sort of values can be overridden with each of these methods.</p>
<h3 id="coq-override"><code>.override</code></h3>
<p><code>.override</code> lets you change arguments to a Coq derivation. In the case of the <code>multinomials</code> package above, <code>.override</code> would let you override arguments like <code>mkCoqDerivation</code>, <code>version</code>, <code>coq</code>, <code>mathcomp</code>, <code>mathcom-finmap</code>, etc.</p>
<p>For example, assuming you have a special <code>mathcomp</code> dependency you want to use, here is how you could override the <code>mathcomp</code> dependency:</p>
<div class="highlight"><pre><span></span><code>multinomials<span class="o">.</span>override <span class="p">{</span>
<span class="ss">mathcomp</span> <span class="o">=</span> my-special-mathcomp<span class="p">;</span>
<span class="p">}</span>
</code></pre></div>
<p>In Nixpkgs, all Coq derivations take a <code>version</code> argument. This can be overridden in order to easily use a different version:</p>
<div class="highlight"><pre><span></span><code>coqPackages<span class="o">.</span>multinomials<span class="o">.</span>override <span class="p">{</span>
<span class="ss">version</span> <span class="o">=</span> <span class="s2">&quot;1.5.1&quot;</span><span class="p">;</span>
<span class="p">}</span>
</code></pre></div>
<p>Refer to <a href="#coq-packages-attribute-sets-coqpackages"></a> for all the different formats that you can potentially pass to <code>version</code>, as well as the restrictions.</p>
<h3 id="coq-overrideCoqDerivation"><code>overrideCoqDerivation</code></h3>
<p>The <code>overrideCoqDerivation</code> function lets you easily change arguments to <code>mkCoqDerivation</code>. These arguments are described in <a href="#coq-packages-attribute-sets-coqpackages"></a>.</p>
<p>For example, here is how you could locally add a new release of the <code>multinomials</code> library, and set the <code>defaultVersion</code> to use this release:</p>
<div class="highlight"><pre><span></span><code>coqPackages<span class="o">.</span>lib<span class="o">.</span>overrideCoqDerivation
<span class="p">{</span>
<span class="ss">defaultVersion</span> <span class="o">=</span> <span class="s2">&quot;2.0&quot;</span><span class="p">;</span>
release<span class="o">.</span><span class="s2">&quot;2.0&quot;</span><span class="o">.</span><span class="ss">sha256</span> <span class="o">=</span> <span class="s2">&quot;1lq8x86vd3vqqh2yq6hvyagpnhfq5wmk5pg2z0xq7b7dbbbhyfkk&quot;</span><span class="p">;</span>
<span class="p">}</span>
coqPackages<span class="o">.</span>multinomials
</code></pre></div>
<h3 id="coq-overrideAttrs"><code>.overrideAttrs</code></h3>
<p><code>.overrideAttrs</code> lets you override arguments to the underlying <code>stdenv.mkDerivation</code> call. Internally, <code>mkCoqDerivation</code> uses <code>stdenv.mkDerivation</code> to create derivations for Coq libraries. You can override arguments to <code>stdenv.mkDerivation</code> with <code>.overrideAttrs</code>.</p>
<p>For instance, here is how you could add some code to be performed in the derivation after installation is complete:</p>
<div class="highlight"><pre><span></span><code>coqPackages<span class="o">.</span>multinomials<span class="o">.</span>overrideAttrs <span class="p">(</span>oldAttrs<span class="p">:</span> <span class="p">{</span>
<span class="ss">postInstall</span> <span class="o">=</span> oldAttrs<span class="o">.</span>postInstall <span class="ow">or</span> <span class="s2">&quot;&quot;</span> <span class="o">+</span> <span class="s s-Multiline">&#39;&#39;</span>
<span class="s s-Multiline"> echo &quot;you can do anything you want here&quot;</span>
<span class="s s-Multiline"> &#39;&#39;</span><span class="p">;</span>
<span class="p">})</span>
</code></pre></div>
</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>
Reference in a new issue View git blame Copy permalink