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")
# «.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

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")






#####
#
# 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-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




#  Local Variables:
#  coding:          utf-8-unix
#  End: