|
Warning: this is an htmlized version!
The original is here, and the conversion rules are here. |
#######
#
# E-scripts on Agda.
#
# Note 1: use the eev command (defined in eev.el) and the
# ee alias (in my .zshrc) to execute parts of this file.
# Executing this file as a whole makes no sense.
# An introduction to eev can be found here:
#
# (find-eev-quick-intro)
# http://angg.twu.net/eev-intros/find-eev-quick-intro.html
#
# Note 2: be VERY careful and make sure you understand what
# you're doing.
#
# Note 3: If you use a shell other than zsh things like |&
# and the for loops may not work.
#
# Note 4: I always run as root.
#
# Note 5: some parts are too old and don't work anymore. Some
# never worked.
#
# Note 6: the definitions for the find-xxxfile commands are on my
# .emacs.
#
# Note 7: if you see a strange command check my .zshrc -- it may
# be defined there as a function or an alias.
#
# Note 8: the sections without dates are always older than the
# sections with dates.
#
# This file is at <http://angg.twu.net/e/agda.e>
# or at <http://angg.twu.net/e/agda.e.html>.
# See also <http://angg.twu.net/emacs.html>,
# <http://angg.twu.net/.emacs[.html]>,
# <http://angg.twu.net/.zshrc[.html]>,
# <http://angg.twu.net/escripts.html>,
# and <http://angg.twu.net/>.
#
#######
# «.mailing-list» (to "mailing-list")
# «.issues» (to "issues")
# «.zulip» (to "zulip")
# «.norell-chapman» (to "norell-chapman")
# «.agda-inst» (to "agda-inst")
# «.agda-inst-dcs» (to "agda-inst-dcs")
# «.agda-inst-bd» (to "agda-inst-bd")
# «.agda-inst-stack» (to "agda-inst-stack")
# «.agda-inst-clai» (to "agda-inst-clai")
# «.agda-inst-bum» (to "agda-inst-bum")
# «.agda-inst-tests» (to "agda-inst-tests")
# «.2024» (to "2024")
# «.plfa-install» (to "plfa-install")
# «.plfa» (to "plfa")
# «.mononoki» (to "mononoki")
# «.plfa-chapters-prince» (to "plfa-chapters-prince")
# «.plfa-git-clone-recurse» (to "plfa-git-clone-recurse")
# «.plfa-library» (to "plfa-library")
# «.numeric-ieee» (to "numeric-ieee")
# «.agdapad» (to "agdapad")
# «.agda-stdlib» (to "agda-stdlib")
# «.agda2-backend» (to "agda2-backend")
# «.cabal-install-agda-utf8» (to "cabal-install-agda-utf8")
# «.cabal-unpack-agda» (to "cabal-unpack-agda")
# «.IO.agda-wrong-place» (to "IO.agda-wrong-place")
# «.agda-stdlib-install» (to "agda-stdlib-install")
# «.agda-debian» (to "agda-debian")
# «.agda-tutorials» (to "agda-tutorials")
# «.agda-mode» (to "agda-mode")
# «.agda2-mode» (to "agda2-mode")
# «.agda-mode-2023» (to "agda-mode-2023")
# «.agda2-mode-map» (to "agda2-mode-map")
# «.agda-mode-cc-cn» (to "agda-mode-cc-cn")
# «.agda-mode-macros» (to "agda-mode-macros")
# «.agda2-send-command» (to "agda2-send-command")
# «.M-,» (to "M-,")
# «.C-c-C-SPC» (to "C-c-C-SPC")
# «.selinger» (to "selinger")
# «.selinger-records» (to "selinger-records")
# «.records» (to "records")
# «.data» (to "data")
# «.import» (to "import")
# «.built-ins» (to "built-ins")
# «.postulates» (to "postulates")
# «.variable» (to "variable")
# «.variable-vs-postulate» (to "variable-vs-postulate")
# «.eek-C-c-C-d» (to "eek-C-c-C-d")
# «.precedence» (to "precedence")
# «.structures» (to "structures")
# «.module-system» (to "module-system")
# «.open-as» (to "open-as")
# «.syntax» (to "syntax")
# «.sort-system» (to "sort-system")
# «.loading» (to "loading")
# «.loading-process» (to "loading-process")
# «.interactive» (to "interactive")
# «.category-theory» (to "category-theory")
# «.agda-categories» (to "agda-categories")
# «.agda-categories-config» (to "agda-categories-config")
# «.carette-wilc» (to "carette-wilc")
# «.heyting-algebra» (to "heyting-algebra")
# «.limpberg-yoneda» (to "limpberg-yoneda")
# «.cabal-agda» (to "cabal-agda")
# «.agda-git» (to "agda-git")
# «.agda-user-manual» (to "agda-user-manual")
# «.could-not-find-ffi» (to "could-not-find-ffi")
# «.agda-path» (to "agda-path")
# «.finite-sets» (to "finite-sets")
# «.lob-paper» (to "lob-paper")
# «.abel-ssft18» (to "abel-ssft18")
# «.brutaldeptypes» (to "brutaldeptypes")
# «.isinverse» (to "isinverse")
# «.agda2-info-buffer» (to "agda2-info-buffer")
# «.cold-introduction» (to "cold-introduction")
# «.failed-to-find-source» (to "failed-to-find-source")
# «.holes» (to "holes")
# «.generating-latex» (to "generating-latex")
# «.poor-mans-way» (to "poor-mans-way")
# «.pivotal» (to "pivotal")
# «.connectives» (to "connectives")
# «.tactics» (to "tactics")
# «.let-and-where» (to "let-and-where")
# «.nonstricttostrict» (to "nonstricttostrict")
# «.decidability» (to "decidability")
# «.universe-levels» (to "universe-levels")
# «.Level» (to "Level")
# «.README.Data.Nat» (to "README.Data.Nat")
# «.lambda» (to "lambda")
# «.extensionality» (to "extensionality")
# «.equality-jan2022» (to "equality-jan2022")
# «.setoids» (to "setoids")
# «.instead-of-a-REPL» (to "instead-of-a-REPL")
# «.agsy» (to "agsy")
# «.cumulativity» (to "cumulativity")
# «.system-F-in-agda» (to "system-F-in-agda")
# «.escardo-hott-uf» (to "escardo-hott-uf")
# «.telescopes» (to "telescopes")
# «.TypeTopology» (to "TypeTopology")
# «.agda-editor-tactics» (to "agda-editor-tactics")
# https://en.wikipedia.org/wiki/Agda_(programming_language)
# https://wiki.portal.chalmers.se/agda/pmwiki.php
# https://wiki.portal.chalmers.se/agda/Main/Download
# https://agda.readthedocs.io/en/latest/index.html
# https://agda.readthedocs.io/en/latest/getting-started/installation.html#installation-from-hackage
# (find-es "coq" "agda")
# (find-es "haskell" "agda2")
#####
#
# mailing-list
# 2021jul02
#
#####
# «mailing-list» (to ".mailing-list")
# https://lists.chalmers.se/mailman/listinfo/agda
# https://lists.chalmers.se/pipermail/agda/ archive
#####
#
# issues
# 2022feb04
#
#####
# «issues» (to ".issues")
# https://github.com/agda/agda/issues
#####
#
# zulip
# 2023jan17
#
#####
# «zulip» (to ".zulip")
# https://wiki.portal.chalmers.se/agda/pmwiki.php
# https://agda.zulipchat.com/
#####
#
# norell-chapman
# 2022oct10
#
#####
# «norell-chapman» (to ".norell-chapman")
# (find-books "__comp/__comp.el" "norell-chapman")
#####
#
# A cleaned-up version of the installation instructions (Debian/Stack/PLFA)
# 2021aug01
#
#####
# «agda-inst» (to ".agda-inst")
* (eepitch-shell)
* (eepitch-kill)
* (eepitch-shell)
# «agda-inst-dcs» (to ".agda-inst-dcs")
# Delete everything from previous installations of Cabal and Stack.
#
# (find-es "cabal" "deleting-cabal-dirs")
# (find-es "stack" "delete-stack")
# (find-fline "~/.cabal/")
# (find-fline "~/.ghc/")
# (find-fline "~/.stack/")
# (find-fline "~/.local/bin/")
rm -Rfv ~/.cabal/
rm -Rfv ~/.ghc/
rm -Rv ~/.stack/
rm -fv ~/.local/bin/stack
rm -fv ~/.local/bin/agda
rm -fv ~/.local/bin/agda-mode
rm -fv /usr/local/bin/stack
# «agda-inst-bd» (to ".agda-inst-bd")
# Install some build dependencies.
#
sudo apt-get build-dep -y agda
sudo apt-get install -y python3-sphinx
sudo apt-get remove -y python3-sphinx
pip3 install sphinx
pip3 install sphinx_rtd_theme
# «agda-inst-stack» (to ".agda-inst-stack")
# Install Stack.
#
# (find-es "stack" "generic-linux")
cd /tmp/
wget -qO- https://get.haskellstack.org/ | sudo sh -s - -d /usr/local/bin/
# «agda-inst-clai» (to ".agda-inst-clai")
# Clone the Agda repository and install agda from it.
#
# (find-es "agda" "agda-git")
# (code-c-d "agdagit" "~/usrc/agda/")
# rm -Rfv ~/usrc/agda/
# cd ~/usrc/
# git clone https://github.com/agda/agda.git
# Version numbers taken from:
# https://plfa.github.io/GettingStarted/#install-agda-using-stack
# https://wiki.portal.chalmers.se/agda/Main/Download
cd ~/usrc/agda/
git clean -dfx
git reset --hard
git checkout v2.6.1.3
export LC_ALL=en_GB.UTF-8
stack install --stack-yaml stack-8.8.3.yaml |& tee osi
stack install --stack-yaml stack-8.8.3.yaml |& tee osi2
#
# (find-agdagitfile "osi")
# «agda-inst-bum» (to ".agda-inst-bum")
# Build the user manual.
#
cd ~/usrc/agda/
make user-manual-html |& tee omumh
make user-manual-pdf |& tee omump
# (code-pdf-page "agdausermanual" "~/usrc/agda/doc/user-manual.pdf")
# (code-pdf-text "agdausermanual" "~/usrc/agda/doc/user-manual.pdf" 4)
# (find-agdagitfile "doc/")
# (find-agdagitfile "doc/user-manual/_build/html/")
# (find-agdausermanualpage)
# (find-agdausermanualtext)
# «agda-inst-tests» (to ".agda-inst-tests")
# Some tests.
#
# (find-angg "AGDA/")
# (find-angg "AGDA/hello.agda")
# (find-angg "AGDA/nats.agda")
# (find-angg "AGDA/hello-world.agda")
#####
#
# 2024
# 2024may09
#
#####
# «2024» (to ".2024")
# https://wiki.portal.chalmers.se/agda/Main/Download
# https://agda.readthedocs.io/en/latest/getting-started/installation.html#installation-from-hackage
# https://hackage.haskell.org/package/Agda-2.6.4.2#readme
* (eepitch-shell)
* (eepitch-kill)
* (eepitch-shell)
sudo apt-get install -y zlib1g-dev libncurses5-dev
cabal update
cabal install Agda
w agda-mode
# (find-fline "~/.cabal/bin/")
# (find-fline "~/.cabal/bin/agda-mode")
(load-file (let ((coding-system-for-read 'utf-8))
(shell-command-to-string "agda-mode locate")))
#####
#
# plfa-install
# 2021jul25
#
#####
# «plfa-install» (to ".plfa-install")
# (find-es "cabal" "deleting-cabal-dirs")
# (find-es "stack" "delete-stack")
# (find-es "agda" "cabal-install-agda-utf8")
# (find-es "agda" "cabal-install-agda-utf8" "/agda/issues/")
# (find-es "agda" "cabal-install-agda-utf8" "export LC_ALL=")
# (find-es "agda" "agda-git")
# (find-es "agda" "plfa-git-clone-recurse")
# (find-es "agda" "numeric-ieee")
* (eepitch-shell)
* (eepitch-kill)
* (eepitch-shell)
export LC_ALL=en_GB.UTF-8
stack update
cd ~/usrc/agda/
git clean -dfx
git reset --hard
git checkout v2.6.1.3
cd ~/usrc/agda/
export LC_ALL=en_GB.UTF-8
stack install --stack-yaml stack-8.8.3.yaml |& tee osi
cd ~/usrc/plfa/
git clean -dfx
git reset --hard
# (find-fline "~/.agda/libraries")
# (find-fline "~/.agda/defaults")
#####
#
# PLFA: Programming Language Foundations in Agda
# 2020jul17
#
#####
# «plfa» (to ".plfa")
# (find-angg ".emacs.agda" "plfa-chapters")
# https://github.com/plfa/plfa.github.io/
# https://plfa.github.io/
# https://plfa.github.io/Preface/
# https://plfa.github.io/GettingStarted/
# https://plfa.github.io/Naturals/
# https://plfa.github.io/Induction/
# https://plfa.github.io/Relations/
# https://plfa.github.io/Equality/
# https://plfa.github.io/Isomorphism/
# http://lists.inf.ed.ac.uk/mailman/listinfo/plfa-interest
# agda-mode setup; agda-mode compile
* (eepitch-shell)
* (eepitch-kill)
* (eepitch-shell)
w agda-mode
agda-mode -h
agda-mode locate
# (find-fline "~/bigsrc/emacs28/src/")
export PATH=$HOME/bigsrc/emacs28/src:$PATH
w emacs
agda-mode setup
agda-mode locate
# (find-fline "~/" " .emacs")
# (find-fline "~/" " .emacs0")
(find-tkdiff "~/.emacs" "/tmp/.emacs")
cp -v ~/.emacs /tmp/
* (eepitch-shell)
* (eepitch-kill)
* (eepitch-shell)
stack upgrade
# (find-es "agda" "agda-git")
# (find-fline "~/usrc/agda/")
# (find-git-links "https://github.com/agda/agda.git" "agda")
* (eepitch-shell)
* (eepitch-kill)
* (eepitch-shell)
cd ~/usrc/agda/
git checkout v2.6.1.3
stack install --stack-yaml stack-8.8.3.yaml |& tee osi
export LC_ALL=en_GB.UTF-8
stack install --stack-yaml stack-8.8.3.yaml |& tee osi2
* (eepitch-shell)
* (eepitch-kill)
* (eepitch-shell)
# (find-es "git" "git-clone-recurse-submodules")
rm -Rfv ~/usrc/plfa/
cd ~/usrc/
git clone --recurse-submodules https://github.com/plfa/plfa.github.io plfa
cd ~/usrc/plfa/
# (code-c-d "plfa" "~/usrc/plfa/")
# (find-plfafile "")
# (find-plfash "find *")
# (find-plfash "find * | grep agda-lib")
# (find-plfafile "standard-library/")
# (find-plfafile "standard-library/" "standard-library.agda-lib")
# (setenv "LC_ALL" "en_GB.UTF-8")
# (find-angg "AGDA/nats.agda")
#####
#
# mononoki
# 2021aug14
#
#####
# «mononoki» (to ".mononoki")
# (find-plfa1page 7 "Optional: using the mononoki font with Emacs")
# (find-plfa1text 7 "Optional: using the mononoki font with Emacs")
# https://packages.debian.org/sid/fonts/fonts-mononoki
# (find-status "fonts-mononoki")
# (find-vldifile "fonts-mononoki.list")
# (find-udfile "fonts-mononoki/")
# (find-efaces "default")
# (find-angg ".emacs" "ee-mononoki")
# (find-efunction 'font)
# (find-efunction 'font "mononoki")
;; default to mononoki
(set-face-attribute 'default nil
:family "mononoki"
;; :height 120
:height 150
:weight 'normal
:width 'normal)
(defun ee-mononoki (&optional ht)
(interactive)
(set-face-attribute 'default nil
:family "mononoki"
:height (or ht 150)
:weight 'normal
:width 'normal))
(defun eejump-17 () (ee-mononoki 120))
(defun eejump-17 () (ee-mononoki 120))
(defun eejump-17 () (ee-mononoki 240))
(set-face-attribute 'default nil
:family "fixed"
:height 98
:weight 'normal
:width 'semicondensed)
#####
#
# Convert some chapters of PLFA to PDFs using Prince
# 2021aug01
#
#####
# «plfa-chapters-prince» (to ".plfa-chapters-prince")
# https://plfa.github.io/
# https://plfa.github.io/Preface/
# https://plfa.github.io/GettingStarted/
# https://plfa.github.io/Naturals/
# https://plfa.github.io/Induction/
# https://plfa.github.io/Relations/
# https://plfa.github.io/Equality/
# https://plfa.github.io/Isomorphism/
https://plfa.github.io/Connectives/
https://plfa.github.io/Negation/
https://plfa.github.io/Quantifiers/
https://plfa.github.io/Decidable/
https://plfa.github.io/Lists/
* (eepitch-shell)
* (eepitch-kill)
* (eepitch-shell)
# (find-efunction 'find-telegram-save-log-links "content: counter(page)")
cat > /tmp/print.css <<'%%%'
body { font-size: 12 !important }
@page {
@bottom {
content: counter(page);
}
}
%%%
mkdir ~/PLFA/
cd /tmp/
cd ~/PLFA/
prince -s /tmp/print.css -o 0._Preface.pdf https://plfa.github.io/Preface/
prince -s /tmp/print.css -o 1._GettingStarted.pdf https://plfa.github.io/GettingStarted/
prince -s /tmp/print.css -o 2._Naturals.pdf https://plfa.github.io/Naturals/
prince -s /tmp/print.css -o 3._Induction.pdf https://plfa.github.io/Induction/
prince -s /tmp/print.css -o 4._Relations.pdf https://plfa.github.io/Relations/
prince -s /tmp/print.css -o 5._Equality.pdf https://plfa.github.io/Equality/
prince -s /tmp/print.css -o 6._Isomorphism.pdf https://plfa.github.io/Isomorphism/
prince -s /tmp/print.css -o 7._Connectives.pdf https://plfa.github.io/Connectives/
prince -s /tmp/print.css -o 8._Negation.pdf https://plfa.github.io/Negation/
prince -s /tmp/print.css -o 9._Quantifiers.pdf https://plfa.github.io/Quantifiers/
prince -s /tmp/print.css -o 10._Decidable.pdf https://plfa.github.io/Decidable/
prince -s /tmp/print.css -o 11._Lists.pdf https://plfa.github.io/Lists/
mkdir ~/PLFA/
cp -iv /tmp/1.pdf ~/PLFA/1._GettingStarted.pdf
cp -iv /tmp/2.pdf ~/PLFA/2._Naturals.pdf
# (find-fline "~/PLFA/")
# (code-pdf-page "plfa1" "~/PLFA/1._GettingStarted.pdf")
# (code-pdf-text "plfa1" "~/PLFA/1._GettingStarted.pdf")
# (code-pdf-page "plfa2" "~/PLFA/2._Naturals.pdf")
# (code-pdf-text "plfa2" "~/PLFA/2._Naturals.pdf")
# (code-pdf-page "plfa3" "~/PLFA/3._Induction.pdf")
# (code-pdf-text "plfa3" "~/PLFA/3._Induction.pdf")
# (code-pdf-page "plfa4" "~/PLFA/4._Relations.pdf")
# (code-pdf-text "plfa4" "~/PLFA/4._Relations.pdf")
# (code-pdf-page "plfa5" "~/PLFA/5._Equality.pdf")
# (code-pdf-text "plfa5" "~/PLFA/5._Equality.pdf")
# (code-pdf-page "plfa6" "~/PLFA/6._Isomorphism.pdf")
# (code-pdf-text "plfa6" "~/PLFA/6._Isomorphism.pdf")
# (code-pdf-page "plfa7" "~/PLFA/7._Connectives.pdf")
# (code-pdf-text "plfa7" "~/PLFA/7._Connectives.pdf")
# (code-pdf-page "plfa8" "~/PLFA/8._Negation.pdf")
# (code-pdf-text "plfa8" "~/PLFA/8._Negation.pdf")
# (code-pdf-page "plfa9" "~/PLFA/9._Quantifiers.pdf")
# (code-pdf-text "plfa9" "~/PLFA/9._Quantifiers.pdf")
# (code-pdf-page "plfa10" "~/PLFA/10._Decidable.pdf")
# (code-pdf-text "plfa10" "~/PLFA/10._Decidable.pdf")
# (code-pdf-page "plfa11" "~/PLFA/11._Lists.pdf")
# (code-pdf-text "plfa11" "~/PLFA/11._Lists.pdf")
# (find-plfa1page)
# (find-plfa1text)
# (find-plfa1text "git checkout v2.6.1.3")
# (find-plfa1page 3 "Agda standard library")
# (find-plfa1text 3 "Agda standard library")
# (find-plfa2page)
# (find-plfa2text)
# (find-plfa3page)
# (find-plfa3text)
# (find-plfa3page 16 "section notation")
# (find-plfa3text 16 "section notation")
# (find-plfa4page)
# (find-plfa4text)
# (find-plfa5page)
# (find-plfa5text)
# (find-plfa6page)
# (find-plfa6text)
# (find-plfa7page)
# (find-plfa7text)
# (find-plfa8page)
# (find-plfa8text)
# (find-plfa9page)
# (find-plfa9text)
# (find-plfa10page)
# (find-plfa10text)
# (find-plfa11page)
# (find-plfa11text)
#####
#
# plfa-git-clone-recurse
# 2021jul25
#
#####
# «plfa-git-clone-recurse» (to ".plfa-git-clone-recurse")
# (find-es "git" "github-cli")
# (find-es "git" "git-clone-recurse-submodules")
* (eepitch-shell)
* (eepitch-kill)
* (eepitch-shell)
rm -Rfv ~/usrc/plfa/
cd ~/usrc/
git clone --recurse-submodules https://github.com/plfa/plfa.github.io plfa
cd ~/usrc/plfa/
git pull
#####
#
# plfa-library
# 2021jul30
#
#####
# «plfa-library» (to ".plfa-library")
# (find-fline "~/.agda/libraries")
# (find-plfash "find *")
# (find-plfash "find * | grep agda-lib")
#####
#
# Could not find module `Numeric.IEEE'
# 2021jul25
#
#####
# «numeric-ieee» (to ".numeric-ieee")
# (find-es "stack" "stack-exec")
# (find-angg "AGDA/test1.agda")
# https://github.com/agda/agda/issues/3619
# https://github.com/agda/agda/issues/2857 better
# https://agda.readthedocs.io/en/v2.6.2/tools/compilers.html
# https://github.com/agda/agda/issues/5486 how do I install ieee754 with stack?
* (eepitch-shell)
* (eepitch-kill)
* (eepitch-shell)
# (find-fline "/tmp/ieee/")
rm -Rv /tmp/ieee/
mkdir /tmp/ieee/
cd /tmp/ieee/
export LC_ALL=en_GB.UTF-8
stack exec --package ieee754 --package text agda
stack install ieee754
stack install text
#####
#
# agdapad
# 2022jan10
#
#####
# «agdapad» (to ".agdapad")
In case you didn't know about it, you can run Agda directly in your
browser without any installation at
https://agdapad.quasicoherent.io/.
If you share a session link with colleagues, you have simultaneous
control over the same Emacs window as a team. However, there are
absolutely no guarantees regarding the availability or permanence of
this service.
#####
#
# agda-stdlib
# 2021jun26
#
#####
# «agda-stdlib» (to ".agda-stdlib")
# (find-fline "~/LOGS/2021jun26.agda")
# (find-fline "~/LOGS/2021jun26.agda" "this works:")
# (find-status "agda-stdlib")
# (find-vldifile "agda-stdlib.list")
# (find-udfile "agda-stdlib/")
# (find-fline "/etc/emacs/site-start.d/60agda-stdlib.el")
# (find-vldifile "agda-stdlib.list" "/usr/share/agda-stdlib/IO")
# (find-fline "/usr/share/agda-stdlib/")
# (find-fline "/usr/share/agda-stdlib/" "IO")
# (find-fline "/etc/emacs/site-start.d/60agda-stdlib.el")
# (load "/etc/emacs/site-start.d/60agda-stdlib.el")
#####
#
# agda2-backend
# 2021jun27
#
#####
# «agda2-backend» (to ".agda2-backend")
# (find-efunctiondescr 'agda2-mode)
# (find-efunctiondescr 'agda2-mode "C-c C-x C-c")
# (find-efunctiondescr 'agda2-mode "C-c C-x C-c" "agda2-compile")
# (find-efunctiondescr 'agda2-compile)
# (find-efunction 'agda2-compile)
# (find-evardescr 'agda2-backend)
# (find-evariable 'agda2-backend)
# (find-books "__comp/__comp.el" "agda")
#####
#
# cabal-install-agda-utf8
# 2021jul02
#
#####
# «cabal-install-agda-utf8» (to ".cabal-install-agda-utf8")
# (find-anggsh "find .cabal | grep Parser | sort")
# (find-anggsh "find .cabal | grep Agda | sort")
# (find-fline "~/.cabal/packages/hackage.haskell.org/Agda/2.6.2/Agda-2.6.2.tar.gz" "Parser/Parser.y")
# https://mail.google.com/mail/ca/u/0/#sent/KtbxLrjCPJVPnGtQCQJlBJNhmZzhZKdsZg
# https://lists.chalmers.se/pipermail/agda/2021/012689.html
# https://github.com/agda/agda/issues/5465
# (find-fline "/etc/locale.gen")
# (find-fline "/etc/locale.gen" :end)
# (find-sh "tail -n 1 /etc/locale.gen")
* (eepitch-shell)
* (eepitch-kill)
* (eepitch-shell)
# (find-es "agda" "cabal-install-agda-utf8")
#
cabal update
export LC_ALL=en_GB.UTF-8
cabal install Agda
Hi list,
the latest version of the Agda Manual from
https://readthedocs.org/projects/agda/downloads/pdf/latest/
mentions a certain error as something that can only happen on M$
Windows. It says:
Warning: If you are installing Agda using Cabal on Windows,
depending on your system locale setting, cabal install Agda may fail
with an error message:
hGetContents: invalid argument (invalid byte sequence)
If this happens, you can try changing the console code page to UTF-8
using the command:
CHCP 65001
I'm on Debian stable and I got something similar. I tried to install
Agda with
cabal update
cabal install Agda
and it failed with:
happy: src/full/Agda/Syntax/Parser/Parser.y: hGetContents: invalid
argument (invalid byte sequence)
cabal: Failed to build Agda-2.6.2. See the build log above for
details.
My default value for $LC_ALL is "C" and the only uncommented line in
my /etc/locale.gen is this one:
en_GB.UTF-8 UTF-8
If I run this
export LC_ALL=en_GB.UTF-8
cabal install Agda
instead of just "cabal install Agda" the compilation succeeds.
Cheers,
Eduardo Ochs
http://angg.twu.net/#eev
http://angg.twu.net/math-b.html
#####
#
# cabal-unpack-agda
# 2021jul03
#
#####
# «cabal-unpack-agda» (to ".cabal-unpack-agda")
* (eepitch-shell)
* (eepitch-kill)
* (eepitch-shell)
mkdir -p ~/.cabal/unpack/
cd ~/.cabal/unpack/
cabal unpack Agda
cabal unpack agda-mode
# (find-fline "~/.cabal/unpack/Agda-2.6.2/")
# (find-fline "~/.cabal/unpack/Agda-2.6.2/src/data/emacs-mode/")
# (code-c-d "agda" "~/.cabal/unpack/Agda-2.6.2/")
# (code-c-d "agdamode" "~/.cabal/unpack/Agda-2.6.2/src/data/emacs-mode/")
# (code-c-d "agdag" "~/.cabal/store/ghc-8.8.4/Agda-2.6.2-b2f8eb43cd09b8b95a6e2958c006bc2f47b9966435e6f21d09b053b958e4fc43/")
# (find-agdafile "")
# (find-agdamodefile "")
# (find-agdagfile "")
# (find-agdagfile "share/emacs-mode/")
* (eepitch-shell)
* (eepitch-kill)
* (eepitch-shell)
cd ~/.cabal/
find * | grep -i stdlib
#####
#
# The cabal-installed Agda on Debian looks for IO.agda in the wrong place
# 2021jul03
#
#####
# «IO.agda-wrong-place» (to ".IO.agda-wrong-place")
# The cabal-installed Agda on Debian looks for IO.agda in the wrong place:
# https://github.com/agda/agda/issues/5466
# (find-agdagfile "share/lib/prim/Agda/Builtin/IO.agda")
This is a follow-up to this issue:
https://github.com/agda/agda/issues/5465
My file ~/AGDA/test1.agda has just this, plus comments:
module test1 where
open import IO
main = run (putStrLn "Hello, World!")
I've tried to compile this test.agda in several ways - for example:
agda -i. test1.agda
GHC_ENVIRONMENT=agda agda -c test1.agda
I always get this error:
Checking test1 (/home/edrx/AGDA/test1.agda).
/home/edrx/AGDA/test1.agda:6,1-15
Failed to find source of module IO in any of the following
locations:
/home/edrx/AGDA/IO.agda
/home/edrx/AGDA/IO.lagda
/home/edrx/.cabal/store/ghc-8.8.4/Agda-2.6.2-b2f8eb43cd09b8b95a6e2958c006bc2f47b9966435e6f21d09b053b958e4fc43/share/lib/prim/IO.agda
/home/edrx/.cabal/store/ghc-8.8.4/Agda-2.6.2-b2f8eb43cd09b8b95a6e2958c006bc2f47b9966435e6f21d09b053b958e4fc43/share/lib/prim/IO.lagda
when scope checking the declaration
open import IO
I do have both an IO.agda and an IO.agdai here, but in a slightly
different path... the first one below is the path of the existing
IO.agda, and the second is the path that agda tries to use:
~/.cabal/store/ghc-8.8.4/Agda-2.6.2-b2f8eb43cd09b8b95a6e2958c006bc2f47b9966435e6f21d09b053b958e4fc43/share/lib/prim/Agda/Builtin/IO.agda
~/.cabal/store/ghc-8.8.4/Agda-2.6.2-b2f8eb43cd09b8b95a6e2958c006bc2f47b9966435e6f21d09b053b958e4fc43/share/lib/prim/IO.agda
can we pretend that this is at least a bug in the documentation, in
the sense that section "Using cabal" in the manual should explain how
to tell agda to look in the right place?
(P.S.: I did some reading and googling and IRCing and testing but I
couldn't find a workaround that works. I am a beginner, sorry =/)
#####
#
# agda-stdlib-install
# 2021jul03
#
#####
# «agda-stdlib-install» (to ".agda-stdlib-install")
# https://github.com/agda/agda-stdlib/blob/master/notes/installation-guide.md
# https://github.com/agda/agda-stdlib/archive/v1.7.tar.gz
# (find-fline "$S/https/github.com/agda/agda-stdlib/archive/")
# (find-fline "$S/https/github.com/agda/agda-stdlib/archive/v1.7.tar.gz")
* (eepitch-shell)
* (eepitch-kill)
* (eepitch-shell)
# (find-fline "~/usrc/agda-stdlib-1.7/")
# (find-fline "~/usrc/agda-stdlib-1.7/notes/installation-guide.md")
rm -Rv ~/usrc/agda-stdlib-1.7/
mkdir ~/usrc/agda-stdlib-1.7/
tar -C ~/usrc/ -xvzf $S/https/github.com/agda/agda-stdlib/archive/v1.7.tar.gz
cd ~/usrc/agda-stdlib-1.7/
cabal install
# (code-c-d "agdastdlib" "~/usrc/agda-stdlib-1.7/")
# (find-agdastdlibfile "")
# (find-agdastdlibfile "notes/installation-guide.md")
# (find-agdastdlibfile "notes/installation-guide.md" ".agda/libraries")
# (find-agdastdlibfile "notes/installation-guide.md" ".agda/defaults")
# Register the standard library with Agda's package system by adding the
# following line to ~/.agda/libraries:
# (find-fline "~/.agda/libraries")
# /home/edrx/usrc/agda-stdlib-1.7/standard-library.agda-lib
# (find-fline "~/.agda/defaults")
# standard-library
# (find-fline "~/LOGS/2021jul03.haskell")
# (find-fline "~/LOGS/2021jul03.haskell" "https://github.com/agda/agda/issues/3619")
# (find-fline "~/LOGS/2021jul03.haskell" "https://github.com/agda/agda/issues/4627")
# (find-angg ".emacs" "agda")
;; (find-agdafile "")
;; (find-agdash "find * | sort")
;; (find-agdagsh "find * | sort")
;; (find-agdamodefile "")
# (find-agdafile "src/data/lib/prim/Agda/Builtin/IO.agda")
# (find-agdafile "src/data/lib/prim/Agda/Builtin/")
<edrx> is this the right place to ask questions about cabal? I'm on
a Debian box that has both agda and agda-mode from Debian -
known to be broken - and an Agda that I've installed from
Cabal... I even had to find a compilation bug and report it,
here:
https://lists.chalmers.se/pipermail/agda/2021/012689.html
<edrx> I am now trying to understand how cabal handle its paths. 1)
is there a better way to specify the path to agda-mode than
"~/.cabal/store/ghc-8.8.4/Agda-2.6.2-b2f8eb43cd09b8b95a6e2958c006bc2f47b9966435e6f21d09b053b958e4fc43/share/emacs-mode/"?
<edrx> 2) when I used the Agda from Debian I had to call it like
this: "agda -i. -i/usr/share/agda-stdlib test1.agda". It
seems that now the path to agda-stdlib should be replaced by
something that points to the agda-stdlib from cabal, that
haven't even been able to locate in ~/.cabal/...
<edrx> any recommended pointers? I am very newbie-ish on those
things - like Haskell, Cabal, and Agda...
<edrx> apologies for asking here, but in #agda people usually take
12 to 24 hours to answer =/
<sclv> you can `cabal unpack agda' to get access to its static
files directly
<sclv> if you don't like the weird place cabal installs em too
<edrx> trying!
<guest61> wait, cabal can manage agda?
<edrx> guest61: it seems so
<edrx> guest61: look here:
https://readthedocs.org/projects/agda/downloads/pdf/latest/#page=12
<edrx> guest61: I am trying to comple the Hello World program
now... did not work, but I reported the reason here:
https://github.com/agda/agda/issues/5466
(edrx)
#####
#
# agda-debian
# 2019mar09
#
#####
# «agda-debian» (to ".agda-debian")
# (find-zsh "installeddebs | sort | grep agda")
# (find-zsh "availabledebs | sort | grep agda")
* (eepitch-shell)
* (eepitch-kill)
* (eepitch-shell)
apti agda agda-mode
# (find-status "agda")
# (find-vldifile "agda.list")
# (find-udfile "agda/")
# (find-status "agda-bin")
# (find-vldifile "agda-bin.list")
# (find-udfile "agda-bin/")
# (find-status "agda-mode")
# (find-vldifile "agda-mode.list")
# (find-udfile "agda-mode/")
# (find-fline "/etc/emacs/site-start.d/50agda.el")
# (find-fline "/etc/emacs/site-start.d/60agda-stdlib.el")
# (find-sitelispfile "agda/")
# (find-status "agda-stdlib")
# (find-vldifile "agda-stdlib.list")
# (find-udfile "agda-stdlib/")
# (find-fline "/usr/share/agda-stdlib/Category/")
# (find-fline "/usr/share/agda-stdlib/Category/Monad.agda")
# (find-status "agda-stdlib-doc")
# (find-vldifile "agda-stdlib-doc.list")
# (find-udfile "agda-stdlib-doc/")
# (find-udfile "agda-stdlib-doc/html/")
# file:///usr/share/doc/agda-stdlib-doc/html/Category.Functor.html
# file:///usr/share/doc/agda-stdlib-doc/html/Category.Functor.Predicate.html
# (find-fline "/etc/emacs/site-start.d/60agda-stdlib.el")
/home/edrx/e(edrx:li)# apti agda agda-mode
[sudo] password for edrx:
Reading package lists... Done
Building dependency tree
Reading state information... Done
The following additional packages will be installed:
agda-bin agda-stdlib agda-stdlib-doc ghc libbsd-dev libghc-agda-dev
libghc-boxes-dev libghc-cpphs-dev libghc-data-hash-dev
libghc-edit-distance-dev libghc-equivalence-dev libghc-geniplate-mirror-dev
libghc-hashable-dev libghc-hashtables-dev libghc-mtl-dev
libghc-old-locale-dev libghc-old-time-dev libghc-parallel-dev
libghc-polyparse-dev libghc-primitive-dev libghc-quickcheck2-dev
libghc-random-dev libghc-split-dev libghc-src-exts-dev
libghc-stmonadtrans-dev libghc-strict-dev libghc-text-dev
libghc-tf-random-dev libghc-transformers-compat-dev
libghc-unordered-containers-dev libghc-vector-dev libghc-zlib-dev
Suggested packages:
ghc-prof ghc-doc haskell-doc llvm-3.5 libghc-agda-doc libghc-boxes-doc
libghc-boxes-prof libghc-cpphs-doc libghc-cpphs-prof libghc-data-hash-doc
libghc-data-hash-prof libghc-edit-distance-doc libghc-edit-distance-prof
libghc-equivalence-doc libghc-equivalence-prof libghc-geniplate-mirror-doc
libghc-geniplate-mirror-prof libghc-hashable-doc libghc-hashable-prof
libghc-hashtables-doc libghc-hashtables-prof libghc-mtl-doc libghc-mtl-prof
libghc-old-locale-doc libghc-old-locale-prof libghc-old-time-doc
libghc-old-time-prof libghc-parallel-doc libghc-parallel-prof
libghc-polyparse-doc libghc-polyparse-prof libghc-primitive-doc
libghc-primitive-prof libghc-quickcheck2-doc libghc-quickcheck2-prof
libghc-random-doc libghc-random-prof libghc-split-doc libghc-split-prof
libghc-src-exts-doc libghc-src-exts-prof libghc-stmonadtrans-doc
libghc-stmonadtrans-prof libghc-strict-doc libghc-strict-prof
libghc-text-doc libghc-text-prof libghc-tf-random-doc libghc-tf-random-prof
libghc-transformers-compat-doc libghc-transformers-compat-prof
libghc-unordered-containers-doc libghc-unordered-containers-prof
libghc-vector-doc libghc-vector-prof libghc-zlib-doc libghc-zlib-prof
The following NEW packages will be installed:
agda agda-bin agda-mode agda-stdlib agda-stdlib-doc ghc libbsd-dev
libghc-agda-dev libghc-boxes-dev libghc-cpphs-dev libghc-data-hash-dev
libghc-edit-distance-dev libghc-equivalence-dev libghc-geniplate-mirror-dev
libghc-hashable-dev libghc-hashtables-dev libghc-mtl-dev
libghc-old-locale-dev libghc-old-time-dev libghc-parallel-dev
libghc-polyparse-dev libghc-primitive-dev libghc-quickcheck2-dev
libghc-random-dev libghc-split-dev libghc-src-exts-dev
libghc-stmonadtrans-dev libghc-strict-dev libghc-text-dev
libghc-tf-random-dev libghc-transformers-compat-dev
libghc-unordered-containers-dev libghc-vector-dev libghc-zlib-dev
0 upgraded, 34 newly installed, 0 to remove and 3 not upgraded.
Need to get 83.6 MB of archives.
After this operation, 771 MB of additional disk space will be used.
Do you want to continue? [Y/n] y
#####
#
# Agda tutorials
# 2019mar09
#
#####
# «agda-tutorials» (to ".agda-tutorials")
# (find-books "__comp/__comp.el" "agda-dtp")
# (find-books "__comp/__comp.el" "agda-verified")
# (find-angg ".emacs.papers" "agda")
# https://wiki.portal.chalmers.se/agda/pmwiki.php
# https://wiki.portal.chalmers.se/agda/pmwiki.php?n=Main.Othertutorials
# https://wiki.portal.chalmers.se/agda/pmwiki.php?n=Main.Documentation
# https://en.wikipedia.org/wiki/Agda_(programming_language)
# http://www.cse.chalmers.se/~peterd/papers/DependentTypesAtWork.pdf
# https://agda.readthedocs.io/en/latest/getting-started/tutorial-list.html
# http://www.cse.chalmers.se/~ulfn/papers/afp08/tutorial.pdf
# http://www.cse.chalmers.se/~ulfn/papers/thesis.pdf
# https://arxiv.org/pdf/1012.4896.pdf MiniAgda: Integrating Sized and Dependent Types
# http://wiki.portal.chalmers.se/agda/uploads/Main.Othertutorials/AgdaOverview2009.pdf
# http://permalink.gmane.org/gmane.comp.lang.agda/1579
# http://www.cl.cam.ac.uk/teaching/0910/L20/
# http://www.cl.cam.ac.uk/teaching/0910/L20/clex1.pdf
# http://www.cl.cam.ac.uk/teaching/0910/L20/clex2a.pdf
# http://www.cl.cam.ac.uk/teaching/0910/L20/clex3.pdf
# http://www.cl.cam.ac.uk/teaching/0910/L20/clex4.pdf
# http://www.cl.cam.ac.uk/~ss368/
#####
#
# The Agda mode for Emacs
# 2010dec17 / 2020aug05
#
#####
# «agda-mode» (to ".agda-mode")
# (find-angg ".emacs" "agda")
# (find-angg ".emacs.agda")
# (find-plfa1page 7 "Using agda-mode in Emacs")
# (find-plfa1text 7 "Using agda-mode in Emacs")
# https://plfa.github.io/GettingStarted/
# https://agda.readthedocs.io/en/v2.6.1/tools/emacs-mode.html
apti elpa-agda2-mode libghc-agda-doc
aptrm agda-mode elpa-agda2-mode
# (find-status "elpa-agda2-mode")
# (find-vldifile "elpa-agda2-mode.list")
# (find-udfile "elpa-agda2-mode/")
# (find-fline "/usr/share/emacs/site-lisp/elpa-src/agda2-mode-2.5.4.1/agda2.el")
# (find-status "agda-mode")
# (find-vldifile "agda-mode.list")
# (find-udfile "agda-mode/")
# (find-status "elpa-agda2-mode")
# (find-vldifile "elpa-agda2-mode.list")
# (find-udfile "elpa-agda2-mode/")
#
# (find-vldifile "elpa-agda2-mode.postinst")
# (find-vldifile "elpa-agda2-mode.prerm")
# (find-status "emacsen-common")
# (find-vldifile "emacsen-common.list")
# (find-udfile "emacsen-common/")
# (find-fline "/usr/lib/emacsen-common/emacs-package-install")
# (find-fline "/usr/lib/emacsen-common/emacs-package-remove")
# (find-fline "/usr/lib/emacsen-common/packages/install/elpa-agda2-mode")
# (find-fline "/usr/lib/emacsen-common/packages/remove/elpa-agda2-mode")
# (find-fline "/usr/share/emacs/site-lisp/elpa-src/agda2-mode-2.5.4.1/")
# (find-fline "/usr/share/emacs/site-lisp/elpa-src/agda2-mode-2.5.4.1/agda2.el")
# (find-fline "/usr/share/emacs/site-lisp/elpa/agda2-mode-2.5.4.1/")
# (find-sitelispfile "agda/")
# (find-sitelispfile "agda/agda-input.el")
# (find-sitelispfile "agda/agda2.el")
# (agda-input-show-translations "Agda")
# (find-efunction 'agda-input-show-translations)
# http://wiki.portal.chalmers.se/agda/pmwiki.php?n=Docs.UnicodeInput
(autoload 'agda2-mode "agda2-mode"
"Major mode for editing Agda files (version e 2)." t)
(add-to-list 'auto-mode-alist '("\\.l?agda\\'" . agda2-mode))
(modify-coding-system-alist 'file "\\.l?agda\\'" 'utf-8)
# https://agda.readthedocs.io/en/v2.5.4/tools/emacs-mode.html
# https://agda.readthedocs.io/en/v2.6.0/tools/emacs-mode.html
#####
#
# agda2-mode
# 2021apr24
#
#####
# «agda2-mode» (to ".agda2-mode")
# (find-angg ".emacs.agda" "agdamodeel")
# (find-agdamodeelfile "")
# (find-agdamodeelfile "agda-input.el")
# (find-epackage-links 'agda2-mode)
# (find-epackage 'agda2-mode)
# https://melpa.org/#/agda2-mode
# (code-c-d "agda2mode" "~/.emacs.d/elpa/agda2-mode-20210220.2039/")
# (find-agda2modefile "")
# (find-agda2modefile "agda2-mode.el" "(defvar agda2-version")
# (find-agda2modefile "agda2-mode.el" "(defvar agda2-version" "2.6.2")
(require 'agda2-mode)
# (find-fline "agda -V")
cabal update
* (eepitch-shell2)
* (eepitch-kill)
* (eepitch-shell2)
cabal help
#####
#
# agda-mode-2023
# 2023jan17
#
#####
# «agda-mode-2023» (to ".agda-mode-2023")
# https://agda.readthedocs.io/en/latest/getting-started/installation.html#step-3-running-the-agda-mode-program
# (find-cabal-links "agda-mode")
#####
#
# agda2-mode-map
# 2021dec12
#
#####
# «agda2-mode-map» (to ".agda2-mode-map")
# (find-agdausermanualpage (+ 4 12) "2.5 Quick Guide to Editing, Type Checking")
# (find-agdausermanualtext (+ 4 12) "2.5 Quick Guide to Editing, Type Checking")
# (find-agdausermanualpage (+ 4 186) "4.4 Emacs Mode")
# (find-agdausermanualtext (+ 4 186) "4.4 Emacs Mode")
-- (find-plfa1page 7 "Using agda-mode in Emacs")
-- (find-plfa1text 7 "Using agda-mode in Emacs")
-- (eek "M-h M-k C-c C-l ;; agda2-load - replace question mark with hole")
-- (eek "M-h M-k C-c C-c ;; agda2-make-case - case split")
-- (eek "M-h M-k C-c C-SPC ;; agda2-give - fill in hole")
-- (eek "M-h M-k C-c C-r ;; agda2-refine - refine with constructor")
-- (eek "M-h M-k C-c C-a ;; agda2-auto-maybe-all - automatically fill in hole")
-- (eek "M-h M-k C-c C-, ;; agda2-goal-and-context - goal type and context")
-- (eek "M-h M-k C-c C-. ;; agda2-goal-and-context-and-inferred - ...type")
-- (eek "M-h M-k M-. ;; agda2-goto-definition-keyboard")
-- (eek "M-h M-k M-, ;; agda2-go-back")
-- (eek "M-h M-k C-c C-d ;; agda2-infer-type-maybe-toplevel")
-- (eek "M-h M-k C-c C-n ;; agda2-compute-normalised-maybe-toplevel")
-- (find-efunctiondescr 'agda2-mode)
-- (find-ekeymapdescr agda2-mode)
-- (find-ekeymapdescr agda2-mode-map)
C-c C-d agda2-infer-type-maybe-toplevel
C-c C-n agda2-compute-normalised-maybe-toplevel
#####
#
# agda2-mode: C-c C-n
# 2021dec31
#
#####
# «agda-mode-cc-cn» (to ".agda-mode-cc-cn")
# (find-efunctiondescr 'agda2-mode)
# (find-ekeymapdescr agda2-mode)
# (find-ekeymapdescr agda2-mode-map)
# (eek "M-h M-k C-c C-n ;; agda2-compute-normalised-maybe-toplevel")
# (find-efunctiondescr 'agda2-compute-normalised-maybe-toplevel)
# (find-efunction 'agda2-compute-normalised-maybe-toplevel)
# (find-efunction 'agda2-compute-normalised)
#####
#
# agda-mode-macros
# 2021dec31
#
#####
# «agda-mode-macros» (to ".agda-mode-macros")
# (find-agdamodeelgrep "grep --color=auto -nH --null -e defmacro *.el")
# (find-eppm '(agda2-maybe-normalised NAME COMMENT CMD WANT))
(defmacro agda2-maybe-normalised (name comment cmd want)
`(agda2-proto-maybe-normalised
,name ,comment ,cmd
("Simplified" "simplified")
("Instantiated" "neither explicitly normalised nor simplified")
("Normalised" "normalised")
(fromgoal ,want)))
#####
#
# agda2-send-command
# 2022feb01
#
#####
# «agda2-send-command» (to ".agda2-send-command")
# (find-ebuffer "*agda2*")
# (find-agdamodeelgrep "grep --color=auto -nH --null -e IOTCM *.el")
# (find-agdamodeelgrep "grep --color=auto -nH --null -e agda2-send-command *.el")
#####
#
# M-,
# 2021dec12
#
#####
# «M-,» (to ".M-,")
# (find-angg ".emacs" "eev-compose-hash")
# (define-key eev-mode-map (kbd "M-,") 'ee-compose-pair)
# (keymap-unset eev-mode-map "M-," 'remove)
# (find-evardescr 'eev-mode-map)
# (find-ekeymapdescr eev-mode-map)
#####
#
# C-c-C-SPC
# 2021dec07
#
#####
# «C-c-C-SPC» (to ".C-c-C-SPC")
# (find-angg ".emacs.agda" "C-c-C-SPC")
# (find-evardescr 'rcirc-track-minor-mode-map)
# (find-evariable 'rcirc-track-minor-mode-map)
# (find-evariable 'rcirc-track-minor-mode-map "C-c C-SPC")
# (find-ekeymapdescr rcirc-track-minor-mode-map)
# (find-efunctiondescr 'define-key)
# (find-efunction 'define-key)
# (find-efunctiondescr 'keymap-set)
# (find-efunction 'keymap-set)
# (find-efunctiondescr 'keymap-unset)
# (find-efunction 'keymap-unset)
(keymap-unset rcirc-track-minor-mode-map "C-c C-SPC" 'remove)
#####
#
# Interactive mode
# 2011nov26
#
#####
# «interactive» (to ".interactive")
# https://lists.chalmers.se/pipermail/agda/2011/002639.html
# http://wiki.portal.chalmers.se/agda/agda.php?n=Main.FeatureRequests
# http://www.cl.cam.ac.uk/teaching/1011/L20/
(defun eepitch-agda () (interactive)
(eepitch-comint "agda" "agda -I"))
# "The interactive mode is no longer supported. Don't complain if it doesn't work."
* (eepitch-agda)
* (eepitch-kill)
* (eepitch-agda)
:?
:eval 2 + 3
#####
#
# Category Theory
# 2019may11
#
#####
# «category-theory» (to ".category-theory")
# https://mathoverflow.net/questions/152497/formalizations-of-category-theory-in-proof-assistants
# https://www.google.com/search?q=yoneda+lemma+agda&oq=yoneda+lemma+agda&aqs=chrome..69i57.3383j0j7&sourceid=chrome&ie=UTF-8
# https://www.schoolofhaskell.com/user/bartosz/understanding-yoneda
# https://wiki.portal.chalmers.se/agda/pmwiki.php?n=Main.Libraries
# https://wiki.portal.chalmers.se/agda/pmwiki.php?n=Main.Libraries?action=download&upname=20110915Category.agda
# http://www.cs.bham.ac.uk/~mhe/yoneda/yoneda.html Martin Escardo' - Literate file ***
# (find-sh "locate -i agda | grep -i category")
#####
#
# agda-categories
# 2022feb07
#
#####
# «agda-categories» (to ".agda-categories")
# https://lists.chalmers.se/pipermail/agda/2020/012424.html agda-categories, a story
# https://lists.chalmers.se/pipermail/agda/2021/012446.html agda-categories, a story
# (find-books "__cats/__cats.el" "hu-carette")
# https://github.com/agda/agda-categories
# https://agda.github.io/agda-categories/
# (find-git-links "https://github.com/agda/agda-categories" "agdacats")
# (code-c-d "agdacats" "~/usrc/agda-categories/")
# (code-c-d "agdacatsc" "~/usrc/agda-categories/src/Categories/")
# (find-agdacatsfile "")
# (find-agdacatsfile "README.md")
# (find-agdacatscsh "find * | sort")
# (find-agdacatscfile "")
# (find-agdacatsfile "src/Categories/")
# (find-agdacatsfile "src/Categories/Category.agda")
# (find-agdacatsfile "src/Categories/Category/")
# (find-agdacatsfile "src/Categories/Category/Core.agda")
# (find-agdacatsfile "src/Categories/Functor.agda" "shortened by inlining")
# (find-agdausermanualpage (+ 4 149) "eta-equality")
# (find-agdausermanualtext (+ 4 149) "eta-equality")
# (find-agdacatsgrep "grep --color=auto -niRH --null -e universal *")
# (find-agdacatsgrep "grep --color=auto -niRH --null -e sets *")
# (find-agdacatsfile "src/Categories/Morphism/Universal.agda")
# (find-agdacatsfile "src/Categories/Category/Construction/Comma.agda")
# (find-agdacatsfile "src/Categories/Object/Initial.agda")
* (eepitch-shell)
* (eepitch-kill)
* (eepitch-shell)
cd ~/usrc/agda-categories/src/Categories/
find * | sort | grep 'agda$' | tee .agdas
# (find-agdacatscgrep "grep --color=auto -niH -e setoid $(cat .agdas)")
# (find-agdacatscgrep "grep --color=auto -niH -e square $(cat .agdas)")
# (find-fline "~/.agda/libraries")
Library 'standard-library-1.7' not found.
Add the path to its .agda-lib file to
'/home/edrx/.agda/libraries'
to install.
Installed libraries:
standard-library-1.6
(/home/edrx/usrc/plfa/standard-library/standard-library.agda-lib)
#####
#
# agda-categories-config
# 2022feb07
#
#####
# «agda-categories-config» (to ".agda-categories-config")
# Replace 1.7 by 1.6 here:
# (find-agdacatsfile "agda-categories.agda-lib")
name: agda-categories
depend: standard-library-1.6
include: src/
# (find-fline "~/.agda/defaults")
standard-library
agda-categories
# (find-fline "~/.agda/libraries")
~/usrc/plfa/standard-library/standard-library.agda-lib
~/usrc/agda-categories/agda-categories.agda-lib
#####
#
# carette-wilc
# 2022sep30
#
#####
# «carette-wilc» (to ".carette-wilc")
# (find-books "__cats/__cats.el" "hu-carette")
# (find-es "agda" "agda-categories")
# (find-youtubedl-links "/sda5/videos/" "Jacques_Carette_-_What_I_learned_from_formalizing_Category_Theory_in_Agda" "VQiQtH47pbM" ".webm" "carettewilc")
# (code-video "carettewilcvideo" "/sda5/videos/Jacques_Carette_-_What_I_learned_from_formalizing_Category_Theory_in_Agda-VQiQtH47pbM.webm")
# (find-carettewilcvideo "0:00")
# https://www.cas.mcmaster.ca/~carette/publications/Learned.pdf
# https://www.cas.mcmaster.ca/~carette/publications.html
# https://github.com/JacquesCarette?tab=repositories
# (code-pdf-page "carettewilc" "$S/https/www.cas.mcmaster.ca/~carette/publications/Learned.pdf")
# (code-pdf-text "carettewilc" "$S/https/www.cas.mcmaster.ca/~carette/publications/Learned.pdf")
# (find-carettewilcpage)
# (find-carettewilctext)
# (find-carettewilcpage 8 "Fewer assumptions lets you see more")
# (find-carettewilctext 8 "Fewer assumptions lets you see more")
#####
#
# heyting-algebra
# 2021nov27
#
#####
# «heyting-algebra» (to ".heyting-algebra")
# (find-angg "AGDA/ha.agda")
# (find-sh "locate HeytingAlgebra")
# (find-agdastdlibsrcfile "Relation/Binary/")
# (find-agdastdlibsrcfile "Relation/Binary/Reasoning/")
# (find-agdastdlibsrcfile "Relation/Binary/Reasoning/PartialOrder.agda")
# (find-agdastdlibsrcfile "Relation/Binary/Lattice.agda")
# (find-agdastdlibsrcfile "Relation/Binary/Properties/")
# (find-agdastdlibsrcfile "Relation/Binary/Properties/HeytingAlgebra.agda")
# (find-agdastdlibsrcfile "Relation/Binary/Properties/JoinSemilattice.agda")
# (find-agdastdlibsrcfile "Relation/Binary/Properties/Lattice.agda")
# (find-agdastdlibsrcfile "Relation/Binary/Construct/Closure/")
# (find-agdastdlibsrcfile "Relation/Binary/Construct/Closure/Equivalence.agda")
# (find-agdastdlibsrcfile "Relation/Binary/Construct/Closure/Reflexive.agda")
# (find-agdastdlibsrcfile "Relation/Binary/Construct/Closure/ReflexiveTransitive.agda")
# (find-agdastdlibsrcfile "Relation/Binary/Construct/Closure/Transitive.agda")
# (find-agdastdlibsrcfile "Relation/Binary/Lattice.agda" "record HeytingAlgebra")
#####
#
# Jannis Limpberg's "Yoneda's Lemma in Excruciating Detail"
# 2019may12
#
#####
# «limpberg-yoneda» (to ".limpberg-yoneda")
# https://limperg.de/posts/2018-07-27-yoneda.html
# https://github.com/JLimperg/cats/blob/8795f417be20e0b2e32351ba32bd185fcf6da3fe/Cats/Functor/Yoneda.agda
;; (find-fline "~/tmp/")
(code-pdf-page "limpberg" "~/tmp/Yoneda_s_Lemma_in_Excruciating_Detail__Jannis_Limpberg.pdf")
(code-pdf-text "limpberg" "~/tmp/Yoneda_s_Lemma_in_Excruciating_Detail__Jannis_Limpberg.pdf")
;; (find-limpbergpage)
;; (find-limpbergtext)
jannis at limpberg.de
www.limpberg.de
https://github.com/JLimperg/cats
* (eepitch-shell)
* (eepitch-kill)
* (eepitch-shell)
# rm -Rfv ~/usrc/cats/
cd ~/usrc/
git clone https://github.com/JLimperg/cats
cd ~/usrc/cats/
# git pull
# (find-fline "~/usrc/")
# (find-fline "~/usrc/cats/")
# (code-c-d "limpbergcats" "~/usrc/cats/")
# (find-limpbergcatsfile "")
# (find-limpbergcatsfile "Cats/Functor/Yoneda.agda")
# (find-gitk "~/usrc/cats/")
#####
#
# Installing Agda via cabal
# 2019may18
#
#####
# «cabal-agda» (to ".cabal-agda")
# (find-es "haskell" "cabal")
# (find-agdausermanualpage (+ 4 5) "2.3.1 Installation from Hackage")
# (find-agdausermanualtext (+ 4 5) "2.3.1 Installation from Hackage")
* (eepitch-shell)
* (eepitch-kill)
* (eepitch-shell)
rm -Rfv ~/.cabal/
cabal update
cabal install Cabal cabal-install
cabal install Agda
cabal install alex
cabal install happy
cabal install Agda
# (find-sh "locate Agda")
* (eepitch-shell)
* (eepitch-kill)
* (eepitch-shell)
cabal update
cabal install Agda
agda-mode setup
which agda
#####
#
# Agda from git
# 2019may20
#
#####
# «agda-git» (to ".agda-git")
# (find-angg ".emacs" "agda")
# (find-es "python" "sphinx-build")
# (code-c-d "agdagit" "~/usrc/agda/")
# (find-agdagitfile "")
# (find-agdagitfile "doc/user-manual/")
# (find-agdagitfile "doc/user-manual/Makefile")
* (eepitch-shell)
* (eepitch-kill)
* (eepitch-shell)
# (find-git-links "https://github.com/agda/agda.git" "agdagit")
# rm -Rfv ~/usrc/agda/
cd ~/usrc/
git clone https://github.com/agda/agda.git
cd ~/usrc/agda/
# git pull origin master
# (code-c-d "agdagit" "~/usrc/agda/")
# (find-agdagitfile "")
# (find-agdagitfile "Makefile")
# (find-agdagitfile "Makefile" "user-manual-pdf")
# (find-agdagitfile "omumh")
# (find-agdagitfile "omump")
# (find-agdagitsh "find * | sort")
# (find-agdagitsh "find * | sort | grep css")
# (find-agdagitsh "find * | sort | grep pdf")
sudo apt-get build-dep -y agda
apti python3-sphinx
aptrm python3-sphinx
pip3 install sphinx
pip3 install sphinx_rtd_theme
cd ~/usrc/agda/
git reset
cd ~/usrc/agda/
make user-manual-html |& tee omumh
make user-manual-pdf |& tee omump
# (find-agdagitfile "omumh")
# (find-agdagitfile "omump")
# (find-agdagitfile "omump" "cp doc/user-manual/_build/latex/Agda.pdf doc/user-manual.pdf")
# (find-agdagitfile "doc/user-manual/_build/latex/")
# (find-agdagitfile "doc/user-manual/_build/latex/Agda.tex")
# (code-c-d "agdausermanual" "~/usrc/agda-user-manual/")
# (find-agdausermanualfile "")
* (eepitch-shell)
* (eepitch-kill)
* (eepitch-shell)
rm -Rv ~/usrc/agda-user-manual/
cp -aiv ~/usrc/agda/doc/user-manual ~/usrc/agda-user-manual
# mkdir ~/usrc/agda-user-manual/
cd ~/usrc/agda-user-manual/
make
make dirhtml |& tee omd
make latex |& tee oml
# (find-man "sphinx-build")
#####
#
# The Agda user manual
# 2019may21
#
#####
# «agda-user-manual» (to ".agda-user-manual")
# (find-books "__comp/__comp.el" "agda")
# https://readthedocs.org/projects/agda/downloads/pdf/latest/
# https://readthedocs.org/projects/agda/downloads/pdf/latest/#page=83
;; (find-fline "~/usrc/agda/doc/")
(code-pdf-page "agdausermanual" "~/usrc/agda/doc/user-manual.pdf")
(code-pdf-text "agdausermanual" "~/usrc/agda/doc/user-manual.pdf" 4)
;; (find-agdausermanualpage)
;; (find-agdausermanualtext)
# (find-agdausermanualpage (+ 4 4) "Dependent types")
# (find-agdausermanualtext (+ 4 4) "Dependent types")
# (find-agdausermanualpage (+ 4 8) "module hello-world where")
# (find-agdausermanualtext (+ 4 8) "module hello-world where")
* (eepitch-shell)
* (eepitch-kill)
* (eepitch-shell)
w agda
locate README.agda
;; (find-anggfile "AGDA/hello.agda")
;; (find-agdausermanualpage (+ 4 3) "1 Overview")
;; (find-agdausermanualpage (+ 4 5) "2 Getting Started")
;; (find-agdausermanualpage (+ 4 5) "2.1 What is Agda?")
;; (find-agdausermanualpage (+ 4 7) "2.2 Prerequisites")
;; (find-agdausermanualpage (+ 4 7) "2.3 Installation")
;; (find-agdausermanualpage (+ 4 11) "2.4 `Hello world' in Agda")
;; (find-agdausermanualpage (+ 4 12) "2.5 Quick Guide to Editing, Type Checking and Compiling Agda Code")
;; (find-agdausermanualpage (+ 4 14) "2.6 A List of Tutorials")
;; (find-agdausermanualpage (+ 4 17) "3 Language Reference")
;; (find-agdausermanualpage (+ 4 17) "3.1 Abstract definitions")
;; (find-agdausermanualpage (+ 4 20) "3.2 Built-ins")
;; (find-agdausermanualpage (+ 4 31) "3.3 Coinduction")
;; (find-agdausermanualpage (+ 4 34) "3.4 Copatterns")
;; (find-agdausermanualpage (+ 4 37) "3.5 Core language")
;; (find-agdausermanualpage (+ 4 37) "3.6 Cubical")
;; (find-agdausermanualpage (+ 4 50) "3.7 Cumulativity")
;; (find-agdausermanualpage (+ 4 51) "3.8 Data Types")
;; (find-agdausermanualpage (+ 4 54) "3.9 Flat Modality")
;; (find-agdausermanualpage (+ 4 55) "3.10 Foreign Function Interface")
;; (find-agdausermanualpage (+ 4 61) "3.11 Function Definitions")
;; (find-agdausermanualpage (+ 4 66) "3.12 Function Types")
;; (find-agdausermanualpage (+ 4 65) "3.13 Generalization of Declared Variables")
;; (find-agdausermanualpage (+ 4 70) "3.14 Implicit Arguments")
;; (find-agdausermanualpage (+ 4 72) "3.15 Instance Arguments")
;; (find-agdausermanualpage (+ 4 78) "3.16 Irrelevance")
;; (find-agdausermanualpage (+ 4 83) "3.17 Lambda Abstraction")
;; (find-agdausermanualpage (+ 4 85) "3.18 Local Definitions: let and where")
;; (find-agdausermanualpage (+ 4 89) "3.19 Lexical Structure")
;; (find-agdausermanualpage (+ 4 93) "3.20 Literal Overloading")
;; (find-agdausermanualpage (+ 4 95) "3.21 Mixfix Operators")
;; (find-agdausermanualpage (+ 4 97) "3.22 Module System")
;; (find-agdausermanualpage (+ 4 102) "3.23 Mutual Recursion")
;; (find-agdausermanualpage (+ 4 104) "3.24 Pattern Synonyms")
;; (find-agdausermanualpage (+ 4 105) "3.25 Positivity Checking")
;; (find-agdausermanualpage (+ 4 107) "3.26 Postulates")
;; (find-agdausermanualpage (+ 4 108) "3.27 Pragmas")
;; (find-agdausermanualpage (+ 4 111) "3.28 Prop")
;; (find-agdausermanualpage (+ 4 113) "3.29 Record Types")
;; (find-agdausermanualpage (+ 4 120) "3.30 Reflection")
;; (find-agdausermanualpage (+ 4 130) "3.31 Rewriting")
;; (find-agdausermanualpage (+ 4 132) "3.32 Run-time Irrelevance")
;; (find-agdausermanualpage (+ 4 134) "3.33 Safe Agda")
;; (find-agdausermanualpage (+ 4 135) "3.34 Sized Types")
;; (find-agdausermanualpage (+ 4 138) "3.35 Syntactic Sugar")
;; (find-agdausermanualpage (+ 4 143) "3.36 Syntax Declarations")
;; (find-agdausermanualpage (+ 4 143) "3.37 Telescopes")
;; (find-agdausermanualpage (+ 4 144) "3.38 Termination Checking")
;; (find-agdausermanualpage (+ 4 146) "3.39 Universe Levels")
;; (find-agdausermanualpage (+ 4 150) "3.40 With-Abstraction")
;; (find-agdausermanualpage (+ 4 162) "3.41 Without K")
;; (find-agdausermanualpage (+ 4 165) "4 Tools")
;; (find-agdausermanualpage (+ 4 165) "4.1 Automatic Proof Search (Auto)")
;; (find-agdausermanualpage (+ 4 168) "4.2 Command-line options")
;; (find-agdausermanualpage (+ 4 178) "4.3 Compilers")
;; (find-agdausermanualpage (+ 4 180) "4.4 Emacs Mode")
;; (find-agdausermanualpage (+ 4 186) "4.5 Literate Programming")
;; (find-agdausermanualpage (+ 4 188) "4.6 Generating HTML")
;; (find-agdausermanualpage (+ 4 188) "4.7 Generating LaTeX")
;; (find-agdausermanualpage (+ 4 205) "4.8 Library Management")
;; (find-agdausermanualpage (+ 4 208) "4.9 Performance debugging")
;; (find-agdausermanualpage (+ 4 209) "4.10 Search Definitions in Scope")
;; (find-agdausermanualpage (+ 4 211) "5 Contribute")
;; (find-agdausermanualpage (+ 4 211) "5.1 Documentation")
;; (find-agdausermanualpage (+ 4 215) "6 The Agda Team and License")
;; (find-agdausermanualpage (+ 4 217) "7 Indices and tables")
;; (find-agdausermanualpage (+ 4 219) "Bibliography")
;; (find-agdausermanualpage (+ 4 221) "Index")
#####
#
# Convert the lines that say "Loading" to elisp hyperlinks
# 2021nov27
#
#####
# «loading» (to ".loading")
* (eepitch-shell)
* (eepitch-kill)
* (eepitch-shell)
cd ~/AGDA/
export LC_ALL=en_GB.UTF-8
agda -v 2 ha.agda |& tee /tmp/o
# «loading-process» (to ".loading-process")
#
grep Loading /tmp/o
grep Loading /tmp/o | awk '{print $2}' | tee /tmp/o2
grep Loading /tmp/o | awk '{print $2}' | tr . / | tee /tmp/o2
cat /tmp/o2 | grep Agda/Builtin | tee /tmp/o2-builtin
cat /tmp/o2 | grep -v Agda/Builtin | tee /tmp/o2-nonbuiltin
cat /tmp/o2-builtin | gsub.lua '.+' '-- (find-agdaprimfile "%0.agda")' | tee /tmp/o3
cat /tmp/o2-nonbuiltin | gsub.lua '.+' '-- (find-agdastdlibsrcfile "%0.agda")' | tee -a /tmp/o3
# (find-fline "/tmp/o3")
#####
#
# Fixing the Could not find module `Data.FFI' error
# 2019jun06
#
#####
# «could-not-find-ffi» (to ".could-not-find-ffi")
# https://www.reddit.com/r/agda/comments/apiudv/having_trouble_setting_up_agda/
# https://raw.githubusercontent.com/agda/agda-stdlib/v0.11/README.agda
# https://www.reddit.com/r/agda/comments/6x1s1f/unable_to_do_io_missing_dataffi_ioffi/
@ https://stackoverflow.com/questions/45969371/agda-unable-to-do-io-missing-data-ffi-io-ffi
# (find-angg "AGDA/hello.agda")
# (find-zsh "installeddebs | sort | grep agda")
# (find-zsh "installeddebs | sort | grep agda | cut -d _ -f 1 | uniq")
# (find-zsh "availabledebs | sort | grep agda")
# (find-man "cut")
Compilation error:
MAlonzo/Code/Agda/Primitive.hs:4:18:
Could not find module `Data.FFI'
Use -v to see a list of the files searched for.
MAlonzo/Code/Agda/Primitive.hs:5:18:
Could not find module `IO.FFI'
Use -v to see a list of the files searched for.
* (eepitch-shell)
* (eepitch-kill)
* (eepitch-shell)
aptrm agda-bin agda-mode agda-stdlib-doc agda-stdlib libghc-agda-dev
sudo apt autoremove
#####
#
# Adding ~/.cabal/bin/ to the PATH (for Agda)
# 2019jun06
#
#####
# «agda-path» (to ".agda-path")
# (find-es "haskell" "cabal-PATH")
# (find-angg ".zshrc" "path")
* (eepitch-shell)
* (eepitch-kill)
* (eepitch-shell)
cd ~/AGDA/
which agda
echo $PATH
export PATH="$HOME/.cabal/bin:$PATH"
echo $PATH
which agda
agda hello.agda
# The lib directory /usr/share/libghc-agda-dev/lib does not exist
#####
#
# finite-sets
# 2019jun11
#
#####
# «finite-sets» (to ".finite-sets")
# http://www.cse.chalmers.se/~nad/repos/lib/src/Data/Fin.agda
# https://stackoverflow.com/questions/7209100/a-definition-for-finite-sets-in-agda
# https://mazzo.li/posts/Lambda.html
# (find-agdagitfile "examples/lib/Data/Fin.agda")
* (eepitch-shell)
* (eepitch-kill)
* (eepitch-shell)
locate Fin.agda
#####
#
# Jason Gross's paper about Loeb's Theorem, written in literate Agda
# 2020mar06
#
#####
# «lob-paper» (to ".lob-paper")
# https://github.com/JasonGross/
# https://github.com/JasonGross/lob
# https://github.com/JasonGross/lob-paper
# https://github.com/JasonGross/lob-paper/blob/master/README-SUPPLEMENTAL.md
# https://jasongross.github.io/lob-paper/nightly/lob.pdf
* (eepitch-shell)
* (eepitch-kill)
* (eepitch-shell)
# rm -Rfv ~/usrc/lob-paper/
cd ~/usrc/
git clone https://github.com/JasonGross/lob-paper
cd ~/usrc/lob-paper/
# (find-fline "~/usrc/lob-paper/")
# (find-gitk "~/usrc/lob-paper/")
# (code-c-d "lobpaper" "~/usrc/lob-paper/")
# (find-lobpaperfile "")
# (find-lobpaperfile "README.md")
# (find-lobpaperfile "README-SUPPLEMENTAL.md")
#####
#
# Tesla Ice Zhang's Cubical non-HOTT (Cold) Introduction
# 2021feb16
#
#####
# «cold-introduction» (to ".cold-introduction")
# https://ice1000.org/
# https://ice1000.org/2019/08-01-Cutt0.html
# https://ice1000.org/2019/08-20-Cutt1.html
# https://ice1000.org/2019/10-01-Cutt2.html
# https://ice1000.org/2019/10-14-Cutt3.html
# https://ice1000.org/lagda/Agda.Primitive.Cubical.html#101
#####
#
# Failed to find source of module IO in any of the following locations
# 2021jun26
#
#####
# «failed-to-find-source» (to ".failed-to-find-source")
# https://github.com/agda/agda/issues/4250
# (find-fline "~/.agda/defaults")
# https://agda.readthedocs.io/en/v2.6.0.1/tools/package-system.html#example-using-the-standard-library
# https://agda.readthedocs.io/en/v2.6.0.1/tools/package-system.html#library-files
# https://agda.readthedocs.io/en/v2.6.0.1/tools/package-system.html#installing-libraries
# https://agda.readthedocs.io/en/v2.6.0.1/tools/package-system.html#using-a-library
# https://lists.chalmers.se/pipermail/agda/2015/008259.html
#####
#
# holes
# 2021jul03
#
#####
# «holes» (to ".holes")
<edrx> does Agda support holes like Idris?
<edrx> anyway, don't worry about that! I need to sleep, thanks
again! =)
<tomsmeding> edrx: it should support that!
<tomsmeding> edrx: I think you're supposed to use agda from an
editor with editor integration; emacs seems to be the
most-supported thing, but atom, or with some
configuration vim, may also work
<tomsmeding> then _ or ? or {!!} are holes
#####
#
# generating-latex
# 2021jul07 / 2022jan10
#
#####
# «generating-latex» (to ".generating-latex")
# (find-angg "AGDA/Logic2.lagda.tex")
# (find-agdausermanualpage (+ 4 197) "4.7 Generating LaTeX")
# (find-agdausermanualtext (+ 4 197) "4.7 Generating LaTeX")
# (find-es "tex" "unicode-math")
# (find-agdagrep "grep --color=auto -nRH --null -e latex *")
# (find-agdafile "src/full/Agda/Interaction/Highlighting/")
# (find-agdafile "src/full/Agda/Interaction/Highlighting/LaTeX/Base.hs")
# https://wiki.portal.chalmers.se/agda/Main/LiterateAgda
# https://tex.stackexchange.com/questions/529907/how-to-set-the-font-which-agda-code-uses
# (code-c-d "agdacats" "~/usrc/agda-categories/")
# (find-agdacatsfile "")
# (find-agdacatsfile "README.md")
# (find-agdacatsfile "src/Categories/")
# (find-agdacatsfile "src/Categories/Category.agda")
# (find-fline "~/usrc/agda-categories/src/")
* (eepitch-shell)
* (eepitch-kill)
* (eepitch-shell)
# (find-fline "/tmp/agdacats/")
# (find-fline "/tmp/agdacats/Categories/")
# (find-fline "/tmp/agdacats/Categories/Category.agda")
# (find-fline "/tmp/agdacats/Categories/Category.tex")
rm -Rv /tmp/agdacats/
mkdir /tmp/agdacats/
cd ~/usrc/agda-categories/src/ && cp -aiv Categories/ /tmp/agdacats/
cd /tmp/agdacats/
cd /tmp/agdacats/Categories/
# (find-es "python" "pygments")
pygmentize -o Category.tex Category.agda
#####
#
# Poor man's way to latex Agda source
# 2021jul07
#
#####
# «poor-mans-way» (to ".poor-mans-way")
# https://lists.chalmers.se/pipermail/agda/2021/012694.html my question
# https://lists.chalmers.se/pipermail/agda/2021/012695.html Jason Hu's answer
# https://lists.chalmers.se/pipermail/agda/2021/012696.html my thanks
# (find-es "tex" "minted")
On Wed, 7 Jul 2021 at 01:09, Jason Hu <fdhzs2010@hotmail.com> wrote:
>
> I am still not sure what exactly you are looking for. What I do is I
> use minted to typeset the code, and I just copy and paste the code
> in. other packages, of course, would also work.
I'll try to do that!
> Or are you asking how to handle the Unicode used in an Agda source?
I guess that minted handles it in the right way, and I'll probably be
able to learn what I need by studying its output. Minted is not
mentioned in the Agda User Manual, and I was looking for pointers...
Thanks!!! =)
Eduardo
#####
#
# Conor McBride's "How to Keep Your Neighbours in Order" (and Pivotal)
# 2021jul10
#
#####
# «pivotal» (to ".pivotal")
# Conor McBride: "How to Keep Your Neighbours in Order"
# (find-books "__comp/__comp.el" "mcbride-pivotal")
# https://personal.cis.strath.ac.uk/conor.mcbride/Pivotal.pdf
# https://github.com/pigworker/Pivotal
#####
#
# Material for Andreas Abel's tutorial at the SSFT 2018
# 2021jul11
#
#####
# «abel-ssft18» (to ".abel-ssft18")
# http://www2.tcs.ifi.lmu.de/~abel/ssft18/index.html
#####
#
# Jan Malakhovski's "Brutal [Meta]Introduction to Dependent Types in Agda"
# 2021jul11
#
#####
# «brutaldeptypes» (to ".brutaldeptypes")
# https://oxij.org/note/BrutalDepTypes/
#####
#
# Peter Selinger's Agda lectures
# 2021oct07
#
#####
# «selinger» (to ".selinger")
# https://www.mathstat.dal.ca/~selinger/agda-lectures/
# https://www.mathstat.dal.ca/~selinger/agda-lectures/video/lecture5-1.mp4 emacs
# https://www.mathstat.dal.ca/~selinger/agda-lectures/files/5/Lambda.agda
# https://www.mathstat.dal.ca/~selinger/agda-lectures/files/5/Equality.agda
# https://www.mathstat.dal.ca/~selinger/agda-lectures/files/5/Bool.agda
# https://www.mathstat.dal.ca/~selinger/agda-lectures/files/5/Nat.agda
# Alternate notation for indexed datatypes:
# https://www.mathstat.dal.ca/~selinger/agda-lectures/video/lecture10-1.mp4
# (code-video "selingeranfidvideo" "$S/https/www.mathstat.dal.ca/~selinger/agda-lectures/video/lecture10-1.mp4")
# (find-selingeranfidvideo "0:00")
# (find-selingeranfidvideo "1:30" "Alternate notation for indexed datatypes")
# (find-selingeranfidvideo "2:22" "that's the definition of equality that we used")
# (find-selingeranfidvideo "3:05" "then the constructors")
# (find-selingeranfidvideo "3:40" "Alternate notation")
# (find-selingeranfidvideo "4:10" "except that this time")
# (find-selingeranfidvideo "5:00" "C-c C-d")
# (find-selingeranfidvideo "7:00" "in Agda 2.4 and earlier they were not equivalent")
# (find-selingeranfidvideo "7:45" "in which the second notation is not possible")
# (find-selingeranfidvideo "7:55" "data Even")
# (find-selingeranfidvideo "8:55" "data Even'")
# (find-selingeranfidvideo "10:05" "this doesn't work because")
# (find-selingeranfidvideo "11:00" "(Isaac's question)")
# (find-selingeranfidvideo "12:30" "then you have to give names here")
# Lecture 10.2 - Namespaces: the Agda module system (30:38)
# https://www.mathstat.dal.ca/~selinger/agda-lectures/video/lecture10-2.mp4
# (code-video "selinger102video" "$S/https/www.mathstat.dal.ca/~selinger/agda-lectures/video/lecture10-2.mp4")
# (find-selinger102video)
# (find-selinger102video "0:00")
# (find-selinger102video "0:50" "Lemma 1")
# (find-selinger102video "1:35" "example:")
# (find-selinger102video "2:20" "data Nat")
# (find-selinger102video "4:20" "define lemmas")
# (find-selinger102video "5:05" "what is the type of plus")
# (find-selinger102video "6:00" "not in scope")
# (find-selinger102video "6:25" "but you can still access")
# (find-selinger102video "7:00" "in maths you sometimes use the same word")
# (find-selinger102video "9:10" "suppose that you are experimenting")
# (find-selinger102video "10:25" "C-c C-d")
# (find-selinger102video "11:30" "the type outside")
# (find-selinger102video "13:55" "a rather trivial theorem")
# (find-selinger102video "14:30" "it is possible to open a module")
# (find-selinger102video "16:05" "every file implicitly defines a module")
# (find-selinger102video "17:50" "import Nat")
# (find-selinger102video "19:10" "open Nat")
# (find-selinger102video "21:00" "a file called Lecture18")
# (find-selinger102video "21:20" "Sarah's question")
# (find-selinger102video "21:50" "Modules.agda")
# (find-selinger102video "25:30" "a namespace is a function from identifiers")
# (find-selinger102video "26:25" "this equality")
# (find-selinger102video "26:45" "nested module")
# (find-selinger102video "27:40" "complain that equality was not defined")
# (find-selinger102video "28:10" "I would have to fully qualify")
# (find-selinger102video "28:35" ".==")
# (find-selinger102video "29:10" "instead of dumping all the identifiers in the toplevel")
# (find-selinger102video "29:20" "open inside another module ")
# Lecture 10.4 - More on modules: private, public, using, renaming, module assignment (29:27)
# https://www.mathstat.dal.ca/~selinger/agda-lectures/video/lecture10-4.mp4
# (code-video "selinger104video" "$S/https/www.mathstat.dal.ca/~selinger/agda-lectures/video/lecture10-4.mp4")
# (find-selinger104video)
# (find-selinger104video "0:00")
# (find-selinger104video "1:40" "a couple more points about modules")
# (find-selinger104video "2:30" "A.x")
# «selinger-records» (to ".selinger-records")
Lecture 12.1 - Motivation for overloading (8:09)
Lecture 12.2 - Overloading, part 1 (3:43)
Lecture 12.3 - Records, part 1 (20:19)
Lecture 12.4 - Student questions (2:19)
Lecture 12.5 - Records, part 2 (26:08)
Lecture 12.6 - Records: Student questions (5:19)
(code-video "sel121video" "$S/https/www.mathstat.dal.ca/~selinger/agda-lectures/video/lecture12-1.mp4")
(code-video "sel122video" "$S/https/www.mathstat.dal.ca/~selinger/agda-lectures/video/lecture12-2.mp4")
(code-video "sel123video" "$S/https/www.mathstat.dal.ca/~selinger/agda-lectures/video/lecture12-3.mp4")
(code-video "sel124video" "$S/https/www.mathstat.dal.ca/~selinger/agda-lectures/video/lecture12-4.mp4")
(code-video "sel125video" "$S/https/www.mathstat.dal.ca/~selinger/agda-lectures/video/lecture12-5.mp4")
(code-video "sel126video" "$S/https/www.mathstat.dal.ca/~selinger/agda-lectures/video/lecture12-6.mp4")
# (find-sel121video "0:00" "Lecture 12.1 - Motivation for overloading (8:09)")
# (find-sel121video "0:00")
# (find-sel122video "0:00" "Lecture 12.2 - Overloading, part 1 (3:43)")
# (find-sel122video "0:00")
# (find-sel123video "0:00" "Lecture 12.3 - Records, part 1 (20:19)")
# (find-sel123video "6:20" "A record is a better way")
# (find-sel123video "11:36" "selinger age = 50")
# (find-sel123video "15:14" "accessor functions")
# (find-sel123video "16:29" "module for the record")
# (find-sel123video "19:03" "you can open it")
# (find-sel123video "19:40" "record module")
# (find-sel123video "0:00")
# (find-sel124video "0:00" "Lecture 12.4 - Student questions (2:19)")
# (find-sel124video "0:00")
# (find-sel125video "0:00" "Lecture 12.5 - Records, part 2 (26:08)")
# (find-sel125video "0:10" "instances and overloading")
# (find-sel125video "2:58" "as an accessor function")
# (find-sel125video "4:30" "selinger .Person.name")
# (find-sel125video "7:05" "C-c C-r")
# (find-sel125video "7:25" "copatterns")
# (find-sel125video "7:40" "Animal.name rosie = \"Rosie\"")
# (find-sel125video "8:55" "open -> omit the prefixes")
# (find-sel125video "0:00")
# (find-sel126video "0:00" "Lecture 12.6 - Records: Student questions (5:19)")
# (find-sel126video "0:00")
#####
#
# records
# 2020jul21
#
#####
# «records» (to ".records")
# (find-angg ".emacs.agda" "recordstutorial")
# https://wiki.portal.chalmers.se/agda/pmwiki.php?n=ReferenceManual.RecordsTutorial
# https://wiki.portal.chalmers.se/agda/pmwiki.php?n=ReferenceManual.RecordsTutorial#syntax
# https://wiki.portal.chalmers.se/agda/pmwiki.php?n=ReferenceManual.RecordsTutorial#Explicitrecordconstructors
# https://wiki.portal.chalmers.se/agda/ReferenceManual/TOC
# How to declare record types
# (find-agdausermanualpage (+ 4 116) "3.29 Record Types")
# (find-agdausermanualtext (+ 4 116) "3.29 Record Types")
# (find-agdastdlibsrcgrep "grep --color=auto -nRH --null -e record *")
* (eepitch-shell)
* (eepitch-kill)
* (eepitch-shell)
# (find-efunction 'find-telegram-save-log-links "content: counter(page)")
cat > /tmp/print.css <<'%%%'
body { font-size: 12 !important }
@page {
@bottom {
content: counter(page);
}
}
%%%
cd /tmp/
prince -s /tmp/print.css -o RecordsTutorial.pdf \
'https://wiki.portal.chalmers.se/agda/pmwiki.php?n=ReferenceManual.RecordsTutorial'
mkdir -p $S/https/wiki.portal.chalmers.se/agda/
cd $S/https/wiki.portal.chalmers.se/agda/
cp -v /tmp/RecordsTutorial.pdf .
#####
#
# data
# 2021dec25
#
#####
# «data» (to ".data")
# (find-agdausermanualpage (+ 4 53) "3.8 Data Types")
# (find-agdausermanualtext (+ 4 53) "3.8 Data Types")
#####
#
# import
# 2021jul30
#
#####
# «import» (to ".import")
# (find-agdausermanualpage (+ 4 101) "3.22.8 Splitting a program over multiple files")
# (find-agdausermanualtext (+ 4 101) "3.22.8 Splitting a program over multiple files")
#####
#
# module-system
# 2021nov27
#
#####
# «module-system» (to ".module-system")
# (find-agdausermanualsrcfile "language/module-system.lagda.rst")
# (find-agdausermanualsrcfile "language/module-system.lagda.rst" "Parameterised modules")
# (find-agdausermanualsrcfile "language/module-system.lagda.rst" "Parameterised modules" "module application")
# (find-agdausermanualpage (+ 4 100) "3.22 Module System")
# (find-agdausermanualtext (+ 4 100) "3.22 Module System")
# (find-agdausermanualpage (+ 4 102) "open Nat1 public")
# (find-agdausermanualtext (+ 4 102) "open Nat1 public")
# (find-agdausermanualpage (+ 4 103) "3.22.7 Parameterised modules")
# (find-agdausermanualtext (+ 4 103) "3.22.7 Parameterised modules")
# (find-agdausermanualpage (+ 4 105) "3.22.9 Datatype modules and record modules")
# (find-agdausermanualtext (+ 4 105) "3.22.9 Datatype modules and record modules")
# (find-agdausermanualpage (+ 4 67) "3.13 Generalization of Declared Variables")
# (find-agdausermanualtext (+ 4 67) "3.13 Generalization of Declared Variables")
# (find-agdagitfile "examples/Introduction/")
# (find-agdagitfile "examples/Introduction/Modules.agda")
# (find-agdagitfile "examples/Introduction/Modules/Parameterised.agda")
#####
#
# open-as
# 2022feb02
#
#####
# «open-as» (to ".open-as")
# (find-agdausermanualpage (+ 4 104) "import M as M'")
# (find-agdausermanualtext (+ 4 104) "import M as M'")
# (find-agdausermanualpage (+ 4 37) "open the record before using its fields")
# (find-agdausermanualtext (+ 4 37) "open the record before using its fields")
# (find-agdausermanualpage (+ 4 100) "has to be opened")
# (find-agdausermanualtext (+ 4 100) "has to be opened")
# (find-agdausermanualpage (+ 4 102) "open A using")
# (find-agdausermanualtext (+ 4 102) "open A using")
#####
#
# isinverse
# 2021dec19
#
#####
# «isinverse» (to ".isinverse")
# (find-agdastdlibsrcgrep "grep --color=auto -niRH --null -e isinverse *")
# (find-agdastdlibsrcfile "Function/Structures.agda" "record IsInverse")
# (find-angg "AGDA/Cats1.agda")
#####
#
# syntax
# 2021dec07
#
#####
# «syntax» (to ".syntax")
# (find-agdastdlibsrcfile "Relation/Binary/PropositionalEquality/Core.agda" "syntax step-≡")
# (find-agdastdlibsrcfile "Relation/Binary/PropositionalEquality/Core.agda" "pattern erefl x =")
# (find-agdausermanualpage (+ 4 107) "3.24 Pattern Synonyms")
# (find-agdausermanualtext (+ 4 107) "3.24 Pattern Synonyms")
# (find-agdausermanualpage (+ 4 148) "3.36 Syntax Declarations")
# (find-agdausermanualtext (+ 4 148) "3.36 Syntax Declarations")
#####
#
# sort-system
# 2021dec27
#
#####
# «sort-system» (to ".sort-system")
# https://agda.readthedocs.io/en/latest/language/sort-system.html
# (find-agdagitfile "")
# (find-es "agda" "sort-system")
#####
#
# agda2-info-buffer
# 2021dec12
#
#####
# «agda2-info-buffer» (to ".agda2-info-buffer")
# (find-evardescr 'mode-line-modes)
# (find-evariable 'mode-line-modes)
# (find-ebuffer "*Agda information*")
# (find-agdamodeelfile "")
# (find-efunctiondescr 'agda2-information-buffer)
# (find-efunction 'agda2-information-buffer)
# (find-agdamodeelgrep "grep --color=auto -nH --null -e agda2-information-buffer *.el")
# (find-evardescr 'agda2-info-buffer)
# (find-efunctiondescr 'agda2-info-buffer)
# (find-efunction 'agda2-info-buffer)
# (find-efunctionpp 'agda2-info-buffer)
# (find-efunctiond 'agda2-info-buffer)
agda2-info-buffer
(find-eppp
(with-current-buffer agda2-info-buffer
(list mode-line-format
mode-line-buffer-identification))
)
#####
#
# connectives
# 2021dec13
#
#####
# «connectives» (to ".connectives")
# (find-agdastdlibsrcfile "")
# (find-angg ".emacs.agda" "plfa7")
# (find-agdagitfile "examples/lib/Logic/Base.agda")
<edrx> hi! I am learning Agda using Wadler's PLFA and Peter
Selinger's lectures. Both Wadler and Selinger _define_ the
logical connectives in their tutorials, but I can't find
references to where these definitions are in Agda's
stdlib... is there a module of Agda that I can import and
that defines _∧_, _∨_, _↔_, etc, for truth-values?
<edrx> any agda users here? asking questions here is usually more
fun than asking them in #agda or #haskell...
<edrx> I am learning Agda from Wadler's PLFA and from Peter
Selinger's lectures, and they both _define_ the logical
connectives
<edrx> is there a standard module that defines _∧_, _∨_, etc, on
truth-values?
<edrx> (btw: I did ask that in #haskell and no one answered)
#####
#
# tactics
# 2021dec13
#
#####
# «tactics» (to ".tactics")
# (find-agdastdlibsrcfile "Tactic/MonoidSolver.agda")
#####
#
# let-and-where
# 2021dec13
#
#####
# «let-and-where» (to ".let-and-where")
# (find-agdausermanualpage (+ 4 86) "3.18 Local Definitions: let and where")
# (find-agdausermanualtext (+ 4 86) "3.18 Local Definitions: let and where")
# (find-agdausermanualpage (+ 4 88) "3.18.2 where-blocks")
# (find-agdausermanualtext (+ 4 88) "3.18.2 where-blocks")
# (find-agdagitsh "find * | grep where")
# (find-agdagitfile "doc/user-manual/")
# (find-agdagitfile "doc/user-manual/language/")
# (find-agdagitfile "doc/user-manual/language/let-and-where.lagda.rst")
# (find-agdagitfile "doc/user-manual/language/let-and-where.lagda.rst" "g ps = e")
-- (find-angg "AGDA/TestWhere.agda")
-- (find-agdastdlibsrcfile "Data/")
-- (find-agdastdlibsrcfile "Data/List.agda")
-- (find-agdastdlibsrcfile "Data/List/Base.agda")
open import Data.List
myreverse : {A : Set} → List A → List A
myreverse {A} xs = rev-append xs []
where
rev-append : List A → List A → List A
rev-append [] ys = ys
rev-append (x ∷ xs) ys = rev-append xs (x ∷ ys)
postulate A B C : Set
postulate f : A → B
postulate g : B → C
h : A → C
h a = let
b = f a
c = g b
in c
-- or:
h : A → C
h a = let
b : B
b = f a
c : C
c = g b
in c
#####
#
# nonstricttostrict
# 2021dec17
#
#####
# «nonstricttostrict» (to ".nonstricttostrict")
# (find-agdastdlibsrcfile "Relation/Binary/Construct/NonStrictToStrict.agda")
# (find-agdausermanualpage (+ 4 31) "3.2.21 Strictness")
# (find-agdausermanualtext (+ 4 31) "3.2.21 Strictness")
# (find-agdausermanualpage (+ 4 114) "3.28 Prop")
# (find-agdausermanualtext (+ 4 114) "3.28 Prop")
# (find-agdastdlibsrcfile "")
# (find-agdastdlibsrcsh "find * | sort")
# (find-agdastdlibsrcsh "find * | sort | grep -i strict")
# (find-agdastdlibsrcfile "Strict.agda")
# (find-agdastackfile "lib/prim/Agda/Builtin/Strict.agda")
# (find-hottpage (+ 12 59) "strict equality of paths")
# (find-hotttext (+ 12 59) "strict equality of paths")
#####
#
# decidability
# 2021dec17
#
#####
# «decidability» (to ".decidability")
# (find-agdastdlibsrcfile "Relation/Nullary.agda")
# (find-agdastdlibsrcfile "Relation/Nullary.agda" "-- Decidability.")
# (find-agdastdlibsrcfile "Relation/Nullary.agda" "README.Decidability")
# (find-agdastdlibsrcfile "Relation/Nullary/Decidable.agda")
# (find-agdastdlibsrcfile "Relation/Binary/Definitions.agda" "-- Decidability")
# (find-agdastdlibsrcsh "find * | sort | grep -i decid")
#####
#
# universe-levels
# 2021dec17
#
#####
# «universe-levels» (to ".universe-levels")
# (find-agdausermanualpage (+ 4 29) "3.2.13 Universe levels")
# (find-agdausermanualtext (+ 4 29) "3.2.13 Universe levels")
#####
#
# Level
# 2021dec24
#
#####
# «Level» (to ".Level")
# (find-agdastdlibsrcfile "Level.agda")
import Level
ℓ₁ : Level.Level
ℓ₁ = Level.suc Level.zero
ℓ₂ : Level.Level
ℓ₂ = Level.suc ℓ₁
#####
#
# built-ins
# 2021dec17
#
#####
# «built-ins» (to ".built-ins")
# (find-agdausermanualpage (+ 4 20) "3.2 Built-ins")
# (find-agdausermanualtext (+ 4 20) "3.2 Built-ins")
#####
#
# postulates
# 2021dec17
#
#####
# «postulates» (to ".postulates")
# (find-es "lean" "axiom")
# (find-es "lean" "postulate")
# (find-agdausermanualpage (+ 4 83) "3.16.3 Irrelevant declarations")
# (find-agdausermanualtext (+ 4 83) "3.16.3 Irrelevant declarations")
# (find-agdausermanualpage (+ 4 110) "3.26 Postulates")
# (find-agdausermanualtext (+ 4 110) "3.26 Postulates")
#####
#
# variable
# 2021dec18
#
#####
# «variable» (to ".variable")
# (find-agdausermanualpage (+ 4 67) "3.13 Generalization of Declared Variables")
# (find-agdausermanualtext (+ 4 67) "3.13 Generalization of Declared Variables")
#####
#
# variable-vs-postulate
# 2021dec27
#
#####
# «variable-vs-postulate» (to ".variable-vs-postulate")
# https://mail.google.com/mail/u/0/#sent/KtbxLthVbWFMVgRvvKcRnqJgXvlMDFcnvB
# https://lists.chalmers.se/pipermail/agda/2021/012832.html my question
# https://lists.chalmers.se/pipermail/agda/2021/012834.html Jesper's answer ***
# https://lists.chalmers.se/pipermail/agda/2021/012838.html my answer
# (find-angg "AGDA/Postulate1.agda")
# Subj: A question on why "postulate" works but "variable" fails
• (eepitch-shell)
• (eepitch-kill)
• (eepitch-shell)
rm -Rv /tmp/test/
mkdir /tmp/test/
cd /tmp/test/
# (find-fline "/tmp/test/")
# (find-fline "/tmp/test/P.agda")
# (find-fline "/tmp/test/V.agda")
Hi! Help! Beginner question!
Let me start with instructions to reproduce the problem.
Put this in the file /tmp/test/P.agda,
--snip--snip--
postulate B₁ : Set
postulate B₂ : (y₁ : B₁) → Set
postulate A₁ : (y₁ : B₁) → (y₂ : B₂ y₁) → Set
postulate A₂ : (y₁ : B₁) → (y₂ : B₂ y₁) → (x₁ : A₁ y₁ y₂) → Set
postulate y₁ : B₁
postulate y₂ : B₂ y₁
postulate x₁ : A₁ y₁ y₂
postulate x₂ : A₂ y₁ y₂ x₁
--snip--snip--
and this in the file /tmp/test/V.agda:
--snip--snip--
variable B₁ : Set
variable B₂ : (y₁ : B₁) → Set
variable A₁ : (y₁ : B₁) → (y₂ : B₂ y₁) → Set
variable A₂ : (y₁ : B₁) → (y₂ : B₂ y₁) → (x₁ : A₁ y₁ y₂) → Set
variable y₁ : B₁
variable y₂ : B₂ y₁
variable x₁ : A₁ y₁ y₂
variable x₂ : A₂ y₁ y₂ x₁
--snip--snip--
When I use the key sequence `C-c C-l' from agda2-mode to load the two
files in the file P.agda everything works, but in V.agda I get an
error whose main message is "Failed to solve the following
constraints"... and in another case in which I was working using
"postulate" worked, but when I used "variable" I got an error that
started with something like "Generalizable variables not allowed
here".
I just spent some hours trying to understand the section 3.14 -
"Generalization of Declared Variables", link:
https://readthedocs.org/projects/agda/downloads/pdf/latest/#page=83
- of the user manual, but it's too terse for me and it has too many
prerequisites, and I am stuck.
So, QUESTION: can you recommend me other places to learn the
distinctions between "postulate" and "variable"?
Thanks in advance!
Eduardo Ochs
http://angg.twu.net/math-b.html
P.S.: I am using Agda 2.6.1.3.
P.P.S.: To be honest I was trying to understand this,
https://wiki.portal.chalmers.se/agda/pmwiki.php?n=ReferenceManual.RecordsTutorial#opening
and to specialize its example to n:=2 and m:=2 and to check if the
"(r : R Δ)" really works, but I have the impression that I need to
understand variables first...
#####
#
# eek-C-c-C-d
# 2021dec27
#
#####
# «eek-C-c-C-d» (to ".eek-C-c-C-d")
# https://mail.google.com/mail/u/0/#sent/QgrcJHsTfQSpNvHvRNKjPDnXLcxPXRZnpZL
# https://lists.chalmers.se/pipermail/agda/2021/012833.html
# Subj: A question about the innards of C-c C-d
• (eepitch-shell)
• (eepitch-kill)
• (eepitch-shell)
rm -Rv /tmp/test/
mkdir /tmp/test/
cd /tmp/test/
# (find-fline "/tmp/test/CcCd.agda")
Hi list,
if we define the function eek in Elisp as:
(defun eek (str)
"Execute STR as a keyboard macro. See `edmacro-mode' for the exact format.\n
An example: (eek \"C-x 4 C-h\")"
(interactive "sKeys: ")
(execute-kbd-macro (read-kbd-macro str)))
and we create a file /tmp/test/T.agda containing this,
--snip--snip--
open import Level
MySet1 : Set₂
MySet1 = Set (Level.suc Level.zero)
postulate B₁ : Set
postulate B₂ : (y₁ : B₁) → Set
postulate A₁ : (y₁ : B₁) → (y₂ : B₂ y₁) → Set
postulate A₂ : (y₁ : B₁) → (y₂ : B₂ y₁) → (x₁ : A₁ y₁ y₂) → Set
record R (y₁ : B₁) (y₂ : B₂ y₁) : MySet1 where
field
x₁ : A₁ y₁ y₂
x₂ : A₂ y₁ y₂ x₁
postulate ay₁ : B₁
postulate ay₂ : B₂ ay₁
postulate ax₁ : A₁ ay₁ ay₂
postulate ax₂ : A₂ ay₁ ay₂ ax₁
postulate ar : R ay₁ ay₂
-- (eek "C-a C-c C-d R RET")
-- (eek "C-a C-c C-d R.x₁ RET")
-- (eek "C-a C-c C-d R.x₂ RET")
-- (eek "C-a C-c C-d ar RET")
-- (eek "C-a C-c C-d R.x₁ SPC ar RET")
--snip--snip--
then the sexps with "eek" work as buttons that can be executed with
C-e C-x C-e, and whose effects are to display the types of the
expressions "R", "R.x₁", "R.x₂", "ar", and "R.x₁ ar" in the second
window... note that the "R.x₁ SPC ar" in the last sexp was sort of
translated to "R.x₁ ar".
I am looking for a better way to do that, but I am having trouble to
understand the innards of the function bound to C-c C-d -
agda2-infer-type-maybe-toplevel - because it uses at least two levels
of macros...
So: suppose that I define foo as:
(defun foo ()
"Running M-x foo in agda2-mode should be equivalent to
typing C-c C-d R.x₁ ar RET"
(interactive)
(bar "R.x₁ ar"))
what is the right way to define bar in a low-level way? Let's suppose
for simplicity that we just want to make this work in situations in
which agda2-infer-type-maybe-toplevel would run
agda2-infer-type-toplevel, and we don't care for the cases in which it
would run agda2-infer-type...
Thanks in advance!
Eduardo Ochs
http://angg.twu.net/#eev
http://angg.twu.net/eev-intros/find-eev-quick-intro.html#3
#####
#
# precedence
# 2021dec17
#
#####
# «precedence» (to ".precedence")
# (find-angg "AGDA/TestStrings.agda")
# (find-agdausermanualpage (+ 4 98) "3.21.1 Precedence")
# (find-agdausermanualtext (+ 4 98) "3.21.1 Precedence")
# (find-agdausermanualpage (+ 4 102) "ExampleRenamingFixity")
# (find-agdausermanualtext (+ 4 102) "ExampleRenamingFixity")
# (find-agdagitfile "examples/Introduction/Operators.agda" "infix 10 if_then_else_")
# (find-agdagitfile "examples/Introduction/Modules.agda" "_++_ :")
# (find-agdastdlibsrcgrep "grep --color=auto -nRH --null -e infix *")
# (find-agdastdlibsrcfile "Data/Integer/Base.agda" "infixl 7 _*_")
# (find-agdastdlibsrcfile "Data/Integer/Base.agda" "infixl 6 _+_")
#####
#
# structures
# 2021dec17
#
#####
# «structures» (to ".structures")
# (find-agdastdlibsrcfile "Relation/Binary/Structures.agda")
#####
#
# README.Data.Nat
# 2021dec18
#
#####
# «README.Data.Nat» (to ".README.Data.Nat")
# (find-plfagrep "grep --color=auto -nH --null -e import src/plfa/part1/*")
# (find-agdastdlibsrcfile "Data/Nat.agda")
# (find-agdastdlibsrcfile "Data/Nat.agda" "See README.Data.Nat")
# (find-sh "locate -i README.Data.Nat")
# (find-sh "locate -i README | grep -i agda")
# (find-anggfile "usrc/agda-stdlib-1.7/README/Data/")
# (find-anggfile "usrc/agda-stdlib-1.7/README/Data/Nat.agda")
# (find-anggfile "usrc/agda-stdlib-1.7/README/Data/Nat/")
# (find-anggfile "usrc/agda-stdlib-1.7/README.agda")
# (find-anggfile "usrc/agda-stdlib-1.7/README.md")
# (find-anggfile "usrc/agda-stdlib-1.7/README/")
#####
#
# lambda
# 2021dec25
#
#####
# «lambda» (to ".lambda")
# (find-agdausermanualpage (+ 4 66) "lambda abstractions")
# (find-agdausermanualtext (+ 4 66) "lambda abstractions")
#####
#
# extensionality
# 2022feb04
#
#####
# «extensionality» (to ".extensionality")
# «equality-jan2022» (to ".equality-jan2022")
# (find-angg ".emacs.agda" "plfa5")
# (find-plfa5page 6 "module -Reasoning {A : Set} where")
# (find-plfafile "src/plfa/part1/Equality.lagda.md")
# (find-plfafile "src/plfa/part1/Equality.lagda.md" "## Leibniz equality")
# https://homepages.inf.ed.ac.uk/wadler/papers/leibniz/leibniz.pdf
# (find-sh "locate PropositionalEquality")
# (find-agdastdlibsrcfile "Relation/Binary/PropositionalEquality.agda")
# (find-agdastdlibsrcfile "Relation/Binary/PropositionalEquality/")
# (find-agdausermanualpage (+ 4 40) "function extensionality")
# (find-agdausermanualtext (+ 4 40) "function extensionality")
# (find-anggfile "AGDA/2022Cats3.agda" "postulate ext")
(let ((default-directory "~/usrc/plfa/standard-library/src/Relation/Binary/"))
(grep "grep --color=auto -nH --null -e ext * */*")
)
open import Level
open import Relation.Binary.PropositionalEquality as Eq
open Eq.≡-Reasoning
# (find-sh "locate Extensionality")
# (find-agdastdlibsrcfile "Axiom/")
# (find-agdastdlibsrcfile "Axiom/Extensionality/")
# (find-agdastdlibsrcfile "Axiom/Extensionality/Heterogeneous.agda")
# (find-agdastdlibsrcfile "Axiom/Extensionality/Propositional.agda")
#####
#
# setoids
# 2022jan29
#
#####
# «setoids» (to ".setoids")
# (find-books "__logic/__logic.el" "wilander")
# https://en.wikipedia.org/wiki/Logical_framework
# https://en.wikipedia.org/wiki/Judgment_(mathematical_logic)
# (find-agdastdlibsrcfile "Relation/Binary/Bundles.agda" "record Setoid")
# (find-plfastdlibgrep "grep --color=auto -nH --null -e Setoid $(find * | grep 'agda$')")
# (find-agdacatscfile "Category/Core.agda" "hom-setoid :")
# (find-agdacatscgrep "grep --color=auto -nH --null -e hom-setoid $(find * | sort | grep 'agda$')")
#####
#
# Instead of a REPL: e-mail to the mailing list
# 2022feb04
#
#####
# «instead-of-a-REPL» (to ".instead-of-a-REPL")
# https://lists.chalmers.se/pipermail/agda/2022/012870.html
Instead of a REPL
Hi all,
this is an answer to the discussion on REPLs on the thread below,
but I thought that this deserves a new thread and a new title...
https://lists.chalmers.se/pipermail/agda/2022/thread.html#12862
https://lists.chalmers.se/pipermail/agda/2022/012862.html
https://lists.chalmers.se/pipermail/agda/2022/012867.html
Here is a simple hack that does most of what I need from a REPL:
http://angg.twu.net/AGDA/find-agdatype.el.html
http://angg.twu.net/AGDA/find-agdatype.el
Here's how to test it. Run this,
rm -Rv /tmp/agdanonrepl/
mkdir /tmp/agdanonrepl/
cd /tmp/agdanonrepl/
wget http://angg.twu.net/AGDA/find-agdatype.el
wget http://angg.twu.net/AGDA/Postulate1.agda
and then this,
(load "/tmp/agdanonrepl/find-agdatype.el")
(find-file "/tmp/agdanonrepl/Postulate1.agda")
then make Agda load Postulate1.agda with `C-c C-l', and execute the
sexps like
-- (find-agdatype ...)
-- (find-agdatypep ...)
-- (find-agdanorm ...)
-- (find-agdanormp ...)
in Postulate1.agda "by hand" and watch what they show in the second
window. The file Postulate1.agda has lots of sexps that depend on eev,
but you can ignore them.
Note that the current version of find-agdatype.el:
1) does not depend on eev (the previous one did),
2) is less than one hour old now,
3) needs better tests and examples.
I hope that this is useful!
All feedback very welcome!
Cheers,
Eduardo Ochs
http://angg.twu.net/eev-agda.html
#####
#
# agsy
# 2022feb26
#
#####
# «agsy» (to ".agsy")
# (find-agdausermanualpage (+ 4 171) "4.1 Automatic Proof Search")
# (find-agdausermanualtext (+ 4 171) "4.1 Automatic Proof Search")
# (find-agdagitfile "")
# (find-agdagitsh "find * | sort")
# (find-agdagitfile "src/full/Agda/Auto/")
# (find-agdagitfile "src/full/Agda/Auto/Auto.hs" "Entry point for Auto tactic (Agsy)")
#####
#
# cumulativity
# 2022mar21
#
#####
# «cumulativity» (to ".cumulativity")
# https://agda.readthedocs.io/en/latest/language/cumulativity.html
# https://cstheory.stackexchange.com/questions/48654/explicit-type-system-with-infinite-non-cumulative-universe-hierarchy
# https://math.stackexchange.com/questions/3145944/why-should-we-adopt-the-cumulative-universe-convention
# http://liamoc.net/posts/2015-09-10-girards-paradox.html
#####
#
# system-F-in-agda
# 2022apr05
#
#####
# «system-F-in-agda» (to ".system-F-in-agda")
# (find-books "__comp/__comp.el" "chapman-systemF")
# (find-angg ".emacs.papers" "wadler-monads")
# https://homepages.inf.ed.ac.uk/wadler/papers/mpc-2019/system-f-in-agda.pdf
#####
#
# escardo-hott-uf
# 2022aug29
#
#####
# «escardo-hott-uf» (to ".escardo-hott-uf")
# https://mail.google.com/mail/u/0/#inbox/FMfcgzGqQJldsfgvrpfgzKfSWXxBksWW
# https://www.cs.bham.ac.uk/~mhe/HoTT-UF-in-Agda-Lecture-Notes/
# http://www.cs.nott.ac.uk/~psztxa/talks/shonan11.pdf
#####
#
# telescopes
# 2022sep11
#
#####
# «telescopes» (to ".telescopes")
# (find-books "__logic/__logic.el" "automath")
# (find-books "__logic/__logic.el" "debruijn-telesc")
# (find-automathpage (+ 21 1005) "Index of subjects")
# (find-automathpage (+ 21 1021) "Telescope")
# (find-automathpage (+ 21 11))
# (find-automathpage (+ 21 21))
# (find-automathpage (+ 21 44))
# (find-automathpage (+ 21 139))
# (find-automathpage (+ 21 158))
# (find-automathpage (+ 21 224))
# (find-automathpage (+ 21 779))
# (find-automathpage (+ 21 984) "[de Bruijn 91a]")
# https://www.win.tue.nl/automath/archive/pdf/aut103.pdf
#####
#
# TypeTopology
# 2022sep20
#
#####
# «TypeTopology» (to ".TypeTopology")
# https://mail.google.com/mail/u/0/#inbox/QgrcJHrtwMDPVBgXBQjxrRtjxcvGRXWlXkv
# https://github.com/martinescardo/TypeTopology
# https://github.com/ayberkt/formal-topology-in-UF
# (find-git-links "https://github.com/martinescardo/TypeTopology" "TypeTopology")
# (code-c-d "formaltopologyinUF" "~/usrc/formal-topology-in-UF/")
# (code-c-d "TypeTopology" "~/usrc/TypeTopology/")
# (find-TypeTopologyfile "")
# (find-TypeTopologygrep "grep --color=auto -niRH --null -e ayberk *")
# (find-formaltopologyinUFfile "")
https://types22.inria.fr/files/2022/06/TYPES_2022_paper_21.pdf
https://odr.chalmers.se/bitstream/20.500.12380/301098/1/CSE%2020-12%20Tosun.pdf
Hi Ayberk,
I do have a question, but it is _very_ naïve... is that ok?
A few months ago I tried to formalize this
http://angg.twu.net/LATEX/2022on-the-missing.pdf#page=41
http://angg.twu.net/math-b.html#2022-md
in Agda with this definition,
SmallCategory = Category zero zero zero
and supposing that both catA and catB are "small categories" in that
sense. I haven't finished that yet - I got busy with other things =( -
but I remember that I struggled for several days just to discover how
to "translate" the carrier of a hom-setoid to a set... or, in other
words, how to specialize the definitions in the library for Category
Theory to obtain cases in which my categories were "classical".
Can something similar be done with your library for Formal Topology
too? It would be very nice to have an example of an Agda file that
would import your library and some, or all, of the definitions here,
https://www.cs.bham.ac.uk/~mhe/HoTT-UF-in-Agda-Lecture-Notes/HoTT-UF-Agda.html
https://www.cs.bham.ac.uk/~mhe/HoTT-UF-in-Agda-Lecture-Notes/HoTT-UF-Agda.html#519696
including, of course, excluded middle - WARNING: I have only read the
introduction of your thesis, and a bit of Martin's notes!... - and
would then show how to define some basic concepts of "classical"
Topology using your library and these extra axioms and definitions...
Cheers, best, etc,
Eduardo
http://angg.twu.net/math-b.html
# https://www.cs.bham.ac.uk/~axt978/
# https://ayberkt.gitlab.io/msc-thesis/thesis-agda-formalisation.tar
# (find-fline "$S/https/ayberkt.gitlab.io/msc-thesis/thesis-agda-formalisation.tar")
* (eepitch-shell)
* (eepitch-kill)
* (eepitch-shell)
# (find-fline "~/usrc/ayberkthesis/")
rm -Rv ~/usrc/ayberkthesis/
mkdir ~/usrc/ayberkthesis/
cd ~/usrc/ayberkthesis/
tar -xvf $S/https/ayberkt.gitlab.io/msc-thesis/thesis-agda-formalisation.tar
#####
#
# agda-editor-tactics
# 2022nov24
#
#####
# «agda-editor-tactics» (to ".agda-editor-tactics")
# (find-epackage-links 'agda-editor-tactics "agdaeditortactics" t)
# (find-epackage 'agda-editor-tactics)
# (code-c-d "agdaeditortactics" "{d}")
# (find-agdaeditortacticsfile "")
# https://github.com/alhassy/next-700-module-systems
# (find-git-links "https://github.com/alhassy/next-700-module-systems" "next700")
# (code-c-d "next700" "~/usrc/next-700-module-systems/")
# (find-next700file "")
# (find-next700file "papers/")
(code-pdf-page "musaalhassydef" "~/usrc/next-700-module-systems/phd-defence.pdf")
(code-pdf-text "musaalhassydef" "~/usrc/next-700-module-systems/phd-defence.pdf")
;; (find-musaalhassydefpage)
;; (find-musaalhassydefpage 10 "levels of exposure")
;; (find-musaalhassydeftext)
(code-pdf-page "musaalhassyphd" "~/usrc/next-700-module-systems/thesis.pdf")
(code-pdf-text "musaalhassyphd" "~/usrc/next-700-module-systems/thesis.pdf")
;; (find-musaalhassyphdpage)
;; (find-musaalhassyphdtext)
http://alhassy.com/next-700-module-systems/papers/GPCE2019_unbundle_slides.pdf
# http://liamoc.net/images/applications.pdf semideciders and hemideciders
;; (find-pdf-page "$S/http/liamoc.net/images/applications.pdf")
;; (find-pdf-text "$S/http/liamoc.net/images/applications.pdf")
(code-pdf-page "oconnoraaps" "$S/http/liamoc.net/images/applications.pdf")
(code-pdf-text "oconnoraaps" "$S/http/liamoc.net/images/applications.pdf")
;; (find-oconnoraapspage)
;; (find-oconnoraapstext)
# http://news.gmane.org/gmane.comp.lang.agda
# http://unit.aist.go.jp/cvs/Agda/main.pdf
To generate highlighted, hyperlinked web pages from source code, run
the following command in a shell:
agda --html --html-dir=<output directory> <root module>
You can change the way in which the code is highlighted by providing
your own CSS file instead of the default one (use the --css option).
http://wiki.portal.chalmers.se/agda/pmwiki.php?n=Main.LiterateAgda
http://wiki.portal.chalmers.se/agda/pmwiki.php?n=ReferenceManual.FindingTheValuesOfImplicitArguments
https://wiki.cse.unsw.edu.au/cs3141/10s1/Agda%20%26%20Haskell%20Resources
# Agda is similar to epigram:
# (find-es "haskell" "epigram")
http://agda.posterous.com/use-agda-input-mode-in-code
https://lists.chalmers.se/pipermail/agda/2011/003420.html
https://twitter.com/ulfnorell?lang=en
https://wiki.portal.chalmers.se/agda/pmwiki.php?n=Main.AgdaVsCoq
http://learnyouanagda.liamoc.net/pages/introduction.html
https://stackoverflow.com/questions/9455786/how-to-learn-agda
https://github.com/jozefg/learn-tt
https://wiki.nikitavoloboev.xyz/programming-languages/agda
# (find-books "__comp/__comp.el" "norell")
https://agda.readthedocs.io/en/latest/language/syntactic-sugar.html#do-notation
https://www.philipzucker.com/metatheory-progress/
https://github.com/pigworker/Samizdat/blob/master/STLCThin.agda
https://github.com/pigworker/Samizdat/blob/master/DeFunct.agda
I'd second the recommendation for Agda:
For something very simple, you can play around in a browser with AgdaPad
There are "getting started" guides at both readthedocs and at the PLFA book site
The old HoTT library was ported to 2.6 by Andrew Swan here
I also second the recommendation for the cubical library
You might also like the formalization accompanying Egbert Rijke's introductory book.
https://agdapad.quasicoherent.io/
https://agda.readthedocs.io/en/v2.6.1.3/getting-started/index.html
https://plfa.github.io/GettingStarted/
https://github.com/awswan/HoTT-Agda
https://github.com/agda/cubical
https://github.com/HoTT-Intro/Agda
SINKAROVS/COCKX: "Choosing is Losing: How to combine the benefits of shallow and deep embeddings through reflection"
https://arxiv.org/abs/2105.10819.pdf
https://area51.stackexchange.com/proposals/126242/proof-assistants
https://paste.tomsmeding.com/dNKEhru6
https://serokell.io/blog/logical-background Bernay's rule
# (find-agdastdlibsrcfile "Function/HalfAdjointEquivalence.agda")
# (find-agdastdlibsrcfile "Function/Related/TypeIsomorphisms.agda")
https://en.wikipedia.org/wiki/Inductive_type#W-_and_M-types
https://ncatlab.org/nlab/show/W-type
https://oylenshpeegul.gitlab.io/blog/posts/20220503/ Compiling Agda
https://www.philipzucker.com/category-theory-in-the-e-automated-theorem-prover/
https://www.philipzucker.com/notes-on-synthesis-and-equation-proving-for-catlab-jl/
https://hal.inria.fr/hal-03814635/document Seventeen Provers under the Hammer
https://github.com/plclub/cbpv-in-agda
Some Reflections on a Computer-aided
Theory Exploration Study in Category Theory
Christoph Benzmüller and Dana Scott
http://aitp-conference.org/2018/slides/CBDS.pdf
https://hustmphrrr.github.io/ Jason Hu
https://hustmphrrr.github.io/mech-type-theories/
https://jesper.cx/posts/agda-core.html
https://hazel.org/
https://news.ycombinator.com/item?id=42004133 Hazel: A live functional programming environment featuring typed holes (hazel.org)
# Local Variables:
# coding: utf-8-unix
# End: