Content-Security-Policy: default-src 'none'
Content-Type: text/plain; charset=UTF-8
Content-Length: 12910
Content-Disposition: inline; filename="agda.scm"
Last-Modified: Thu, 06 Feb 2025 20:28:34 GMT
Expires: Sun, 04 Feb 2035 20:28:34 GMT
ETag: "4afe583b2e8750bfc35f61269865f7741e96cb7f"

;;; GNU Guix --- Functional package management for GNU
;;; Copyright © 2018 Alex ter Weele <alex.ter.weele@gmail.com>
;;; Copyright © 2018 Ricardo Wurmus <rekado@elephly.net>
;;; Copyright © 2018 Alex Vong <alexvong1995@gmail.com>
;;; Copyright © 2018, 2022 Tobias Geerinckx-Rice <me@tobias.gr>
;;; Copyright © 2018 John Soo <jsoo1@asu.edu>
;;; Copyright © 2019 Ludovic Courtès <ludo@gnu.org>
;;; Copyright © 2023 Josselin Poiret <dev@jpoiret.xyz>
;;;
;;; This file is part of GNU Guix.
;;;
;;; GNU Guix is free software; you can redistribute it and/or modify it
;;; under the terms of the GNU General Public License as published by
;;; the Free Software Foundation; either version 3 of the License, or (at
;;; your option) any later version.
;;;
;;; GNU Guix is distributed in the hope that it will be useful, but
;;; WITHOUT ANY WARRANTY; without even the implied warranty of
;;; MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
;;; GNU General Public License for more details.
;;;
;;; You should have received a copy of the GN</td></tr></table>
<table class='tabs'><tr><td>
<a href='/guix/about/'>about</a><a href='/guix/'>summary</a><a href='/guix/refs/?id=d58ee08dffe99b8fb0523cf2eeec1f337cccfb88'>refs</a><a href='/guix/log/etc/indent-code.el.in'>log</a><a class='active' href='/guix/tree/etc/indent-code.el.in?id=d58ee08dffe99b8fb0523cf2eeec1f337cccfb88'>tree</a><a href='/guix/commit/etc/indent-code.el.in?id=d58ee08dffe99b8fb0523cf2eeec1f337cccfb88'>commit</a><a href='/guix/diff/etc/indent-code.el.in?id=d58ee08dffe99b8fb0523cf2eeec1f337cccfb88'>diff</a></td><td class='form'><form class='right' method='get' action='/guix/log/etc/indent-code.el.in'>
<input type='hidden' name='id' value='d58ee08dffe99b8fb0523cf2eeec1f337cccfb88'/><select name='qt'>
<option value='grep'>log msg</option>
<option value='author'>author</option>
<option value='committer'>committer</option>
<option value='range'>range</option>
</select>
<input class='txt' type='search' size='10' name='q' value=''/>
<input type='submit' value='search'/>
</form>
</td></tr></table>
<div class='path'>path: <a href='/guix/tree/?id=d58ee08dffe99b8fb0523cf2eeec1f337cccfb88'>root</a>/<a href='/guix/tree/etc?id=d58ee08dffe99b8fb0523cf2eeec1f337cccfb88'>etc</a>/<a href='/guix/tree/etc/indent-code.el.in?id=d58ee08dffe99b8fb0523cf2eeec1f337cccfb88'>indent-code.el.in</a></div><div class='content'>blob: 6102b5d1ab7baaaea2824fdf114c2831480d559c (<a href='/guix/about/etc/indent-code.el.in?id=d58ee08dffe99b8fb0523cf2eeec1f337cccfb88'>about</a>) (<a href='/guix/plain/etc/indent-code.el.in?id=d58ee08dffe99b8fb0523cf2eeec1f337cccfb88'>plain</a>)
<table summary='blob content' class='blob'>
<tr><td class='linenumbers'><pre><a id='n1' href='#n1'>1</a>
<a id='n2' href='#n2'>2</a>
<a id='n3' href='#n3'>3</a>
<a id='n4' href='#n4'>4</a>
<a id='n5' href='#n5'>5</a>
<a id='n6' href='#n6'>6</a>
<a id='n7' href='#n7'>7</a>
<a id='n8' href='#n8'>8</a>
<a id='n9' href='#n9'>9</a>
<a id='n10' href='#n10'>10</a>
<a id='n11' href='#n11'>11</a>
<a id='n12' href='#n12'>12</a>
<a id='n13' href='#n13'>13</a>
<a id='n14' href='#n14'>14</a>
<a id='n15' href='#n15'>15</a>
<a id='n16' href='#n16'>16</a>
<a id='n17' href='#n17'>17</a>
<a id='n18' href='#n18'>18</a>
<a id='n19' href='#n19'>19</a>
<a id='n20' href='#n20'>20</a>
<a id='n21' href='#n21'>21</a>
<a id='n22' href='#n22'>22</a>
<a id='n23' href='#n23'>23</a>
<a id='n24' href='#n24'>24</a>
<a id='n25' href='#n25'>25</a>
<a id='n26' href='#n26'>26</a>
<a id='n27' href='#n27'>27</a>
<a id='n28' href='#n28'>28</a>
<a id='n29' href='#n29'>29</a>
<a id='n30' href='#n30'>30</a>
<a id='n31' href='#n31'>31</a>
<a id='n32' href='#n32'>32</a>
<a id='n33' href='#n33'>33</a>
<a id='n34' href='#n34'>34</a>
<a id='n35' href='#n35'>35</a>
<a id='n36' href='#n36'>36</a>
<a id='n37' href='#n37'>37</a>
<a id='n38' href='#n38'>38</a>
<a id='n39' href='#n39'>39</a>
<a id='n40' href='#n40'>40</a>
<a id='n41' href='#n41'>41</a>
<a id='n42' href='#n42'>42</a>
<a id='n43' href='#n43'>43</a>
<a id='n44' href='#n44'>44</a>
<a id='n45' href='#n45'>45</a>
<a id='n46' href='#n46'>46</a>
<a id='n47' href='#n47'>47</a>
<a id='n48' href='#n48'>48</a>
<a id='n49' href='#n49'>49</a>
<a id='n50' href='#n50'>50</a>
<a id='n51' href='#n51'>51</a>
<a id='n52' href='#n52'>52</a>
<a id='n53' href='#n53'>53</a>
<a id='n54' href='#n54'>54</a>
<a id='n55' href='#n55'>55</a>
<a id='n56' href='#n56'>56</a>
<a id='n57' href='#n57'>57</a>
<a id='n58' href='#n58'>58</a>
<a id='n59' href='#n59'>59</a>
<a id='n60' href='#n60'>60</a>
<a id='n61' href='#n61'>61</a>
<a id='n62' href='#n62'>62</a>
<a id='n63' href='#n63'>63</a>
<a id='n64' href='#n64'>64</a>
<a id='n65' href='#n65'>65</a>
<a id='n66' href='#n66'>66</a>
<a id='n67' href='#n67'>67</a>
<a id='n68' href='#n68'>68</a>
<a id='n69' href='#n69'>69</a>
<a id='n70' href='#n70'>70</a>
<a id='n71' href='#n71'>71</a>
<a id='n72' href='#n72'>72</a>
<a id='n73' href='#n73'>73</a>
<a id='n74' href='#n74'>74</a>
<a id='n75' href='#n75'>75</a>
<a id='n76' href='#n76'>76</a>
<a id='n77' href='#n77'>77</a>
<a id='n78' href='#n78'>78</a>
<a id='n79' href='#n79'>79</a>
<a id='n80' href='#n80'>80</a>
<a id='n81' href='#n81'>81</a>
<a id='n82' href='#n82'>82</a>
<a id='n83' href='#n83'>83</a>
<a id='n84' href='#n84'>84</a>
<a id='n85' href='#n85'>85</a>
<a id='n86' href='#n86'>86</a>
<a id='n87' href='#n87'>87</a>
<a id='n88' href='#n88'>88</a>
<a id='n89' href='#n89'>89</a>
<a id='n90' href='#n90'>90</a>
<a id='n91' href='#n91'>91</a>
<a id='n92' href='#n92'>92</a>
<a id='n93' href='#n93'>93</a>
<a id='n94' href='#n94'>94</a>
<a id='n95' href='#n95'>95</a>
<a id='n96' href='#n96'>96</a>
<a id='n97' href='#n97'>97</a>
<a id='n98' href='#n98'>98</a>
<a id='n99' href='#n99'>99</a>
<a id='n100' href='#n100'>100</a>
<a id='n101' href='#n101'>101</a>
<a id='n102' href='#n102'>102</a>
<a id='n103' href='#n103'>103</a>
<a id='n104' href='#n104'>104</a>
<a id='n105' href='#n105'>105</a>
<a id='n106' href='#n106'>106</a>
<a id='n107' href='#n107'>107</a>
<a id='n108' href='#n108'>108</a>
<a id='n109' href='#n109'>109</a>
<a id='n110' href='#n110'>110</a>
<a id='n111' href='#n111'>111</a>
<a id='n112' href='#n112'>112</a>
<a id='n113' href='#n113'>113</a>
<a id='n114' href='#n114'>114</a>
</pre></td>
<td class='lines'><pre><code>#!@EMACS@ --script
;;; indent-code.el --- Run Emacs to indent a package definition.

;; Copyright © 2017 Alex Kost &lt;alezost@gmail.com&gt;
;; Copyright © 2017 Ludovic Courtès &lt;ludo@gnu.org&gt;

;; This file is part of GNU Guix.

;; GNU Guix is free software; you can redistribute it and/or modify
;; it under the terms of the GNU General Public License as published by
;; the Free Software Foundation, either version 3 of the License, or
;; (at your option) any later version.

;; GNU Guix is distributed in the hope that it will be useful,
;; but WITHOUT ANY WARRANTY; without even the implied warranty of
;; MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
;; GNU General Public License for more details.

;; You should have received a copy of the GNU General Public License
;; along with this program.  If not, see &lt;http://www.gnu.org/licenses/&gt;.

;;; Commentary:

;; This scripts indents the given file or package definition in the specified
;; file using Emacs.

;;; Code:

;; Load Scheme indentation rules from ".dir-locals.el".
(with-temp-buffer
  (scheme-mode)
  (let ((default-directory (file-name-as-directory load-file-name))
        (enable-local-variables :all))
    (hack-dir-local-variables)
    (hack-local-variables-apply)))

;; Add indentation info for Scheme constructs that are not Guix-specific.
;; This is normally provided by Geiser but this file is for people who may not
;; be running Geiser, so we just copy it here (from 'geiser-syntax.el').
(defmacro guix-syntax--scheme-indent (&amp;rest pairs)
  `(progn ,@(mapcar (lambda (p)
                      `(put ',(car p) 'scheme-indent-function ',(cadr p)))
                    pairs)))

(guix-syntax--scheme-indent
 (and-let* 1)
 (case-lambda 0)
 (catch defun)
 (class defun)
 (dynamic-wind 0)
 (guard 1)
 (let*-values 1)
 (let-values 1)
 (let/ec 1)
 (letrec* 1)
 (match 1)
 (match-lambda 0)
 (match-lambda* 0)
 (match-let scheme-let-indent)
 (match-let* 1)
 (match-letrec 1)
 (opt-lambda 1)
 (parameterize 1)
 (parameterize* 1)
 (receive 2)
 (require-extension 0)
 (syntax-case 2)
 (test-approximate 1)
 (test-assert 1)
 (test-eq 1)
 (test-equal 1)
 (test-eqv 1)
 (test-group-with-cleanup 1)
 (test-runner-on-bad-count! 1)
 (test-runner-on-bad-end-name! 1)
 (test-runner-on-final! 1)
 (test-runner-on-group-begin! 1)
 (test-runner-on-group-end! 1)
 (test-runner-on-test-begin! 1)
 (test-runner-on-test-end! 1)
 (test-with-runner 1)
 (unless 1)
 (when 1)
 (while 1)
 (with-exception-handler 1)
 (with-syntax 1))


(pcase command-line-args-left
  (`(,file-name ,package-name)
   ;; Indent the definition of PACKAGE-NAME in FILE-NAME.
   (find-file file-name)
   (goto-char (point-min))
   (if (re-search-forward (concat "^(define\\(-public\\) +"
                                  package-name)
                          nil t)
       (let ((indent-tabs-mode nil))
         (beginning-of-defun)
         (indent-sexp)
         (save-buffer)
         (message "Done!"))
     (error "Package '%s' not found in '%s'"
            package-name file-name)))
  (`(,file-name)
   ;; Indent all of FILE-NAME.
   (find-file file-name)
   (let ((indent-tabs-mode nil))
     (indent-region (point-min) (point-max))
     (save-buffer)
     (message "Done!")))
  (x
   (error "Usage: indent-code.el FILE [PACKAGE]")))

;;; indent-code.el ends here
</code></pre></td></tr></table>
</div> <!-- class=content -->
                         <div class=footer>generated by
                             <a href="https://git.zx2c4.com/cgit/about/">
                                 cgit
                             </a>
                         </div>
                        </div> <!-- id=cgit -->
</body>
</html>
ches "agda-categories-remove-incompatible-flags.patch"
                                       "agda-categories-use-find.patch"
                                       "agda-categories-use-stdlib-1.7.3.patch"))))
    (build-system agda-build-system)
    (arguments
     (list
      #:gnu-and-haskell? #t
      #:phases
      #~(modify-phases %standard-phases
          (replace 'build
            (lambda _
              (invoke "make"))))))
    (propagated-inputs
     (list agda-stdlib))
    (synopsis "New Categories library for Agda")
    (description "A new Categories library for Agda")
    (home-page "https://github.com/agda/agda-categories")
    (license license:expat)))

(define-public agda-cubical
  (package
    (name "agda-cubical")
    (version "0.6")
    (source (origin
              (method git-fetch)
              (uri (git-reference
                    (url "https://github.com/agda/cubical.git")
                    (commit (string-append "v" version))))
              (file-name (git-file-name name version))
              (sha256
               (base32
                "0zq0z328zcjmm43mrv2ks27i1dnbylcf8mhzja2hd4gvz1kq1ays"))))
    (build-system agda-build-system)
    (arguments
     (list
      #:gnu-and-haskell? #t
      #:phases
      #~(modify-phases %standard-phases
          (replace 'build
            (lambda _
              (invoke "make"))))))
    (synopsis "Standard library for Cubical Agda")
    (description "A standard library for Cubical Agda, comparable to
agda-stdlib but using cubical methods.")
    (home-page "https://github.com/agda/cubical")
    (license license:expat)))

(define-public agda-1lab
  ;; Upstream doesn't do releases (yet).  Use a commit that builds with 2.6.4,
  ;; since they use Agda HEAD.
  (let* ((revision "2")
         (commit "549fdb1c948a975e90e70f871993a4a4239aa280"))
    (package
      (name "agda-1lab")
      (version (git-version "0.0" revision commit))
      (source
       (origin
         (method git-fetch)
         (uri (git-reference
               (url "https://github.com/plt-amy/1lab.git")
               (commit commit)))
         (file-name (git-file-name name version))
         (sha256
          (base32
           "1k4zj8dibyplakpxaw4a8hpsaqhakynjb83dqxrva4h4ssj6gkqj"))))
      (build-system agda-build-system)
      (arguments
       ;; Check files individually first, to avoid running out of heap :(
       (list #:plan '(("src/.+/.+\\.lagda\\.md$")
                      ("src/index\\.lagda\\.md$"))))
      (synopsis "Reference resource for mathematics done in Homotopy Type Theory")
      (description "A formalised, cross-linked reference resource for
mathematics done in Homotopy Type Theory.  Unlike the HoTT book, the 1lab is
not a “linear” resource: Concepts are presented as a directed graph, with
links indicating dependencies.")
      (home-page "https://1lab.dev")
      (license license:agpl3))))
