|
Warning: this is an htmlized version!
The original is here, and the conversion rules are here. |
#######
#
# E-scripts on Idris.
#
# 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/idris.e>
# or at <http://angg.twu.net/e/idris.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")
# «.slack» (to "slack")
# «.long-story-short» (to "long-story-short")
# «.idris-ct» (to "idris-ct")
# «.idris-ct-install» (to "idris-ct-install")
# «.idris-ct-import» (to "idris-ct-import")
# «.idris-load-packages» (to "idris-load-packages")
# «.pruviloj» (to "pruviloj")
# «.statebox» (to "statebox")
# «.idris-on-debian» (to "idris-on-debian")
# «.idris-on-debian-msg» (to "idris-on-debian-msg")
# «.idris-git» (to "idris-git")
# «.idris-git-docs» (to "idris-git-docs")
# «.idris-mode» (to "idris-mode")
# «.idris-mode-git» (to "idris-mode-git")
# «.idris2-mode» (to "idris2-mode")
# «.idris-docs-online» (to "idris-docs-online")
# «.idris-doc-complete» (to "idris-doc-complete")
# «.tutorial-samples» (to "tutorial-samples")
# «.meleiro» (to "meleiro")
# «.nikolaj-kuntner» (to "nikolaj-kuntner")
# «.obj-vs-obs-cat1» (to "obj-vs-obs-cat1")
# «.Pair» (to "Pair")
# «.the» (to "the")
# «.idris-heyting-algebra» (to "idris-heyting-algebra")
# «.import» (to "import")
# «.preorders» (to "preorders")
# «.Either» (to "Either")
# «.lowercase» (to "lowercase")
# «.bytecode» (to "bytecode")
# «.command-line» (to "command-line")
# «.holes» (to "holes")
# «.indentation» (to "indentation")
# «.bradytdd» (to "bradytdd")
# «.bradys-book-examples» (to "bradys-book-examples")
# «.postulate» (to "postulate")
# «.snap-install-idris2» (to "snap-install-idris2")
# «.idris2» (to "idris2")
# «.idris2-docs» (to "idris2-docs")
# «.idris2-git» (to "idris2-git")
# «.learn-idris.net» (to "learn-idris.net")
# «.jake-gillberg» (to "jake-gillberg")
# «.preorder-reasoning» (to "preorder-reasoning")
# «.eckart» (to "eckart")
# «.juan-HAJ-dec-2020» (to "juan-HAJ-dec-2020")
https://en.wikipedia.org/wiki/Idris_(programming_language)
https://www.idris-lang.org/
http://docs.idris-lang.org/en/latest/
http://docs.idris-lang.org/en/latest/tutorial/index.html
https://groups.google.com/forum/#!forum/idris-lang
https://github.com/idris-lang/Idris-dev/
https://github.com/idris-lang/Idris-dev/wiki/Installation-Instructions
https://github.com/idris-lang/Idris-dev/wiki/Idris-on-Ubuntu
https://github.com/idris-lang/Idris-dev/wiki/Idris-on-Debian
#####
#
# mailing-list
# 2019nov10
#
#####
# «mailing-list» (to ".mailing-list")
# (to "obj-vs-obs-cat1")
# https://www.idris-lang.org/news/
# https://groups.google.com/forum/#!forum/idris-lang
# https://groups.google.com/forum/#!topic/idris-lang/6FMWA02GKJM adjunctions
# https://groups.google.com/forum/#!topic/idris-lang/RzpBsPYKMFA my msg on installing
#####
#
# slack
# 2019nov10
#
#####
# «slack» (to ".slack")
# https://groups.google.com/forum/#!topic/idris-lang/YQji4nw-ciw
# https://functionalprogramming.slack.com
#####
#
# Long story short: what I did to install idris and idris-ct
# 2019oct19
#
#####
# «long-story-short» (to ".long-story-short")
* (eepitch-shell)
* (eepitch-kill)
* (eepitch-shell)
# (find-es "haskell" "cabal")
sudo apt-get install cabal-install
# (find-es "haskell" "cabal-PATH")
# (find-angg ".zshrc" "cabal")
export PATH=$HOME/.cabal/bin:$PATH
# (find-es "cabal" "installing-idris")
cabal install Idris
# (find-es "idris" "idris-git")
# rm -Rfv ~/usrc/Idris-dev/
cd ~/usrc/
git clone http://github.com/idris-lang/Idris-dev
cd ~/usrc/Idris-dev/
make user_doc_pdf |& tee omudp
# (find-angg ".emacs" "idris" "idrisdocc")
# (find-es "idris" "idris-mode")
# (find-epackage 'idris-mode)
# (find-es "idris" "idris-ct")
rm -Rfv ~/usrc/idris-ct/
cd ~/usrc/
git clone https://github.com/statebox/idris-ct
cd ~/usrc/idris-ct/
* (eepitch-shell)
* (eepitch-kill)
* (eepitch-shell)
cd ~/usrc/idris-ct/
idris --libdir
idris --docdir
idris --listlibs
# (find-es "idris" "idris-ct-install")
# (find-fline "~/usrc/idris-ct/idris-ct.ipkg")
cd ~/usrc/idris-ct/
time nice \
idris --V2 --install idris-ct.ipkg |& oiii
idris --listlibs
#####
#
# idris-ct
# 2019jul01
#
#####
# «idris-ct» (to ".idris-ct")
# (find-angg ".emacs" "idris-ct")
# (find-books "__cats/__cats.el" "genovese")
# http://www.cs.ox.ac.uk/ACT2019/preproceedings/ACT%202019%20list%20of%20Papers.pdf
# http://www.cs.ox.ac.uk/ACT2019/preproceedings/ACT2019%20programme.pdf
# 21 Fabrizio Genovese, Alex Gryzlov, Jelle Herold, Marco Perone, Erik
# Post and André Videla idris-ct: A library to do category theory
# in Idris
# https://www.youtube.com/watch?v=MmjBUwnZQZU
# https://github.com/statebox/idris-ct
# (find-git-links "https://github.com/statebox/idris-ct" "idrisct")
# (find-efunction 'find-git-links)
* (eepitch-shell)
* (eepitch-kill)
* (eepitch-shell)
rm -Rfv ~/usrc/idris-ct/
cd ~/usrc/
git clone https://github.com/statebox/idris-ct
cd ~/usrc/idris-ct/
# (find-fline "~/usrc/")
# (find-fline "~/usrc/idris-ct/")
make pdf |& tee omp
# (find-idrisctfile "omp")
# (code-c-d "idrisct" "~/usrc/idris-ct/")
# (find-idrisctfile "")
# (find-gitk "~/usrc/idris-ct/")
# (find-idrisctsh "find * | sort")
# (find-idrisctfile "src/Basic/")
# (find-idrisctfile "src/Basic/Category.lidr")
# (find-idrisctfile "src/Basic/Category.lidr" "record Category where")
# (find-idrisctfile "src/Basic/Functor.lidr")
# (find-idrisctfile "src/Basic/NaturalTransformation.lidr")
# (find-idrisctgrep "grep --color -niRH --null -e believe *")
# (find-idrisctpage 4 "2.2 The module Functor")
# (find-idriscttext 4 "2.2 The module Functor")
#####
#
# idris-ct-install
# 2019oct19
#
#####
# «idris-ct-install» (to ".idris-ct-install")
# (find-idrisctfile "idris-ct.ipkg")
# (find-fline "~/LOGS/2019oct19.idris")
* (eepitch-shell)
* (eepitch-kill)
* (eepitch-shell)
# (find-fline "~/usrc/idris-ct/idris-ct.ipkg")
# (find-fline "~/usrc/idris-ct/")
# (find-fline "~/usrc/idris-ct/oiii")
# (find-fline "~/usrc/idris-ct/oiidi")
cd ~/usrc/idris-ct/
time nice \
idris --V2 --install idris-ct.ipkg |& tee oiii
time nice \
idris --V2 --installdoc idris-ct.ipkg |& tee oiidi
* (eepitch-shell)
* (eepitch-kill)
* (eepitch-shell)
# (find-sh "idris --help")
# (find-sh "idris --help" "--install IPKG")
# (find-sh "idris --help" "--libdir ")
# (find-sh "idris --help" "--listlibs ")
# (find-sh "idris --help" "-p,--package ARG")
idris --libdir
idris --listlibs
idris --docdir
# (find-idrisdoccpage (+ 1 33) "1.6.2 Using Package files")
# (find-idrisdocctext (+ 1 33) "1.6.2 Using Package files")
# (find-idrisdoccpage (+ 1 159) "6.3 Packages")
# (find-idrisdocctext (+ 1 159) "6.3 Packages")
# (find-idrisdoccpage (+ 1 161) "idris -p test Main.idr")
# (find-idrisdocctext (+ 1 161) "idris -p test Main.idr")
#####
#
# idris-ct-import
# 2019nov20
#
#####
# «idris-ct-import» (to ".idris-ct-import")
# (find-sh "idris --help" "--listlibs ")
# (find-sh "idris --help" "-p,--package ARG")
# https://emacs.stackexchange.com/questions/42399/how-to-load-an-idris-file-that-depends-on-a-package
#####
#
# idris-load-packages
# 2019nov20
#
#####
# «idris-load-packages» (to ".idris-load-packages")
# (find-efunction 'idris-set-idris-load-packages)
# (find-evardescr 'idris-load-packages)
# (setq idris-load-packages '("idris-ct"))
idris-load-packages
# (find-angg "IDRIS/Yoneda.idr")
* (eepitch-shell)
* (eepitch-kill)
* (eepitch-shell)
cd ~/IDRIS/
idris -p idris-ct Yoneda.idr
#####
#
# pruviloj
# 2019oct19
#
#####
# «pruviloj» (to ".pruviloj")
# (find-sh "idris --listlibs")
# (find-sh "locate pruviloj")
# (find-fline "~/.cabal/share/x86_64-linux-ghc-8.0.1/idris-1.3.2/docs/pruviloj/")
# (find-fline "~/.cabal/share/x86_64-linux-ghc-8.0.1/idris-1.3.2/libs/pruviloj/")
# (find-fline "~/.cabal/share/x86_64-linux-ghc-8.0.1/idris-1.3.2/libs/pruviloj/")
# (find-idrisgitfile "libs/pruviloj/")
# (find-idrisgitfile "libs/pruviloj/README.txt")
#####
#
# statebox
# 2019jul02
#
#####
# «statebox» (to ".statebox")
# https://statebox.org/about/
# https://arxiv.org/pdf/1906.07629.pdf The Mathematical Specification of the Statebox Language
;; (find-fline "$S/https/arxiv.org/pdf/")
;; (find-fline "$S/https/arxiv.org/pdf/" "1906.07629.pdf")
;; (find-pdf-page "$S/https/arxiv.org/pdf/1906.07629.pdf")
;; (find-pdf-text "$S/https/arxiv.org/pdf/1906.07629.pdf")
# https://github.com/statebox/idris-ct
# https://blog.statebox.org/fun-with-categories-70c64649b8e0
# https://blog.statebox.org/concrete-categories-af444d5f055e
# https://blog.statebox.org/fun-with-functors-95e4e8d60d87
# https://blog.statebox.org/programming-is-just-an-example-6bc6bacb7b72
;; (find-fline "$S/https/blog.statebox.org/")
;; (find-code-pdf-links "$S/https/blog.statebox.org/Concrete categories - Statebox.pdf" "idrisctcc")
;; (find-code-pdf-links "$S/https/blog.statebox.org/Fun with Categories - Statebox.pdf" "idrisctfc")
;; (find-code-pdf-links "$S/https/blog.statebox.org/Fun with functors - Statebox.pdf" "idrisctff")
(code-pdf-page "idrisctfc" "$S/https/blog.statebox.org/Fun with Categories - Statebox.pdf")
(code-pdf-text "idrisctfc" "$S/https/blog.statebox.org/Fun with Categories - Statebox.pdf")
(code-pdf-page "idrisctcc" "$S/https/blog.statebox.org/Concrete categories - Statebox.pdf")
(code-pdf-text "idrisctcc" "$S/https/blog.statebox.org/Concrete categories - Statebox.pdf")
(code-pdf-page "idrisctff" "$S/https/blog.statebox.org/Fun with functors - Statebox.pdf")
(code-pdf-text "idrisctff" "$S/https/blog.statebox.org/Fun with functors - Statebox.pdf")
;; (find-idrisctfcpage)
;; (find-idrisctfctext)
;; (find-idrisctccpage)
;; (find-idrisctcctext)
;; (find-idrisctffpage)
;; (find-idrisctfftext)
# (find-idrisctfcpage 6 "record Category where")
# (find-idrisctfctext 6 "record Category where")
# (find-idrisctfile "src/Basic/Category.lidr" "record Category where")
# (find-idrisctpage 1 "record Category where")
# (find-idriscttext 1 "record Category where")
#####
#
# idris-on-debian
# 2019jul04
#
#####
# «idris-on-debian» (to ".idris-on-debian")
# (find-es "haskell" "haskell-platform")
# https://github.com/idris-lang/Idris-dev/wiki/Idris-on-Debian
# (find-angg ".zshrc" "cabal")
# (find-status "cabal-install")
# (find-vldifile "cabal-install.list")
# (find-udfile "cabal-install/")
* (eepitch-shell)
* (eepitch-kill)
* (eepitch-shell)
# (find-fline "~/.cabal/")
rm -Rfv ~/.cabal/
sudo apt-get install haskell-platform
sudo apt-get install libncurses5-dev
cabal update
cabal install idris
# (find-man "cabal")
cabal update
cabal sandbox init
cabal install idris
* (eepitch-shell)
* (eepitch-kill)
* (eepitch-shell)
sudo apt install haskell-platform
sudo apt install libncurses5-dev
mkdir Idris
cd Idris
cabal update
cabal sandbox init
cabal install idris
#####
#
# idris-on-debian-msg
# 2020jan04
#
#####
# «idris-on-debian-msg» (to ".idris-on-debian-msg")
# https://groups.google.com/forum/#!topic/idris-lang/RzpBsPYKMFA my msg on installing
# https://mail.google.com/mail/ca/u/0/#inbox/FMfcgxwGCbKKhfMJfggRMqnBVrlfwhpq
Hi Eric,
when I installed Idris for the first time a few months ago (obs: I'm a
beginner!) most recipes that I tried didn't work... the one that
worked for me was the first one in this page,
https://github.com/idris-lang/Idris-dev/wiki/Idris-on-Debian
and I just tested it again and found that if I drop the steps that
don't make much sense to me it still works! So:
# I added this step to remove all the non-Debian stuff from the
# previous installation...
rm -Rfv ~/.cabal/
sudo apt-get install haskell-platform
sudo apt-get install libncurses5-dev
# Why does the page recommend this?
# I commented these steps out...
#mkdir Idris
#cd Idris
cabal update
# I don't understand sandboxes well, so let me try to work
# without them. Commented out!
#cabal sandbox init
cabal install idris
# Obs: the last thing that "cabal install idris" does is:
# Downloading idris-1.3.2...
# Configuring idris-1.3.2...
# Building idris-1.3.2...
# The step "Building idris-1.3.2..." takes about 20 minutes in my
# machine!
# Test:
export PATH=$HOME/.cabal/bin:$PATH
idris
# Yaaaaay! =)
Debian and Ubuntu are quite similar... can you try this on your
virtual machine with the most recent version of Ubuntu that you have
and tell us if it works?
Cheers,
Eduardo Ochs
http://angg.twu.net/#eev
http://angg.twu.net/emacsconf2019.html
Warning: could not create symlinks in /home/edrx/.cabal/bin for cheapskate,
idris, idris-codegen-c, idris-codegen-javascript, idris-codegen-node because
the files exist there already and are not managed by cabal. You can create
symlinks for these executables manually if you wish. The executable files have
been installed at /home/edrx/.cabal/bin/cheapskate,
/home/edrx/.cabal/bin/idris, /home/edrx/.cabal/bin/idris-codegen-c,
/home/edrx/.cabal/bin/idris-codegen-javascript,
/home/edrx/.cabal/bin/idris-codegen-node
#####
#
# idris-git
# 2019sep22
#
#####
# «idris-git» (to ".idris-git")
# (find-angg ".emacs" "idris")
# (find-es "python" "sphinx-build")
# http://github.com/idris-lang/Idris-dev
# (find-git-links "http://github.com/idris-lang/Idris-dev" "idrisgit")
* (eepitch-shell)
* (eepitch-kill)
* (eepitch-shell)
rm -Rfv ~/usrc/Idris-dev/
cd ~/usrc/
git clone http://github.com/idris-lang/Idris-dev
* (eepitch-shell)
* (eepitch-kill)
* (eepitch-shell)
cd ~/usrc/Idris-dev/
export PAGER=cat
git branch --list -a
git for-each-ref
git log --oneline --graph --all -20
git reset --hard
git clean -dfx
cd ~/usrc/Idris-dev/
git checkout v1.0
git checkout v1.1.0
git checkout v1.2.0
git checkout v1.3.0
git checkout v1.3.1
git checkout v1.3.2
# git checkout v1.3.3
# (find-idrisgitgrep "grep --color -nRH --null -e documentation-complete *")
# (find-idrisgitgrep "grep --color -nRH --null -e 'Preorder reasoning' *")
# (find-idrisgitgrep "grep --color -nRH --null -e '={' $(find * | sort | grep rst)")
# (find-idrisgitfile "docs/conf.py" "idris-documentation-complete.tex")
# (find-idrisgitsh "find * | sort")
# (find-idrisgitsh "find * | sort | grep idris-documentation-complete")
# (find-idrisgitsh "find * | sort | grep rst")
# export PATH=/usr/local/texlive/2020/bin/x86_64-linux:$PATH
cd ~/usrc/Idris-dev/
make user_doc_pdf |& tee omudp
# (find-idrisgitfile "omudp")
# (find-idrisgitfile "docs/_build/latex/idris-documentation-complete.tex")
I\def\textPi{Pi}
I\def\textlambda{lambda}
R
# (find-fline "~/usrc/")
# (find-fline "~/usrc/Idris-dev/")
# (find-gitk "~/usrc/Idris-dev/")
# (code-c-d "idrisgit" "~/usrc/Idris-dev/")
# (find-idrisgitfile "")
# (find-idrisgitfile "README.md")
# (find-idrisgitfile "INSTALL.md")
# (find-idrisgitfile "Makefile")
# (find-idrisgitfile "Makefile" "user_doc_pdf:")
# (find-idrisgitfile "docs/Makefile")
# (find-idrisgitfile "docs/Makefile" "latexpdf:")
# (find-idrisgitfile "docs/tutorial/")
# (find-idrisgitfile "docs/reference/")
# (find-idrisgitfile "docs/_build/latex/")
# (find-idrisgitsh "find * | sort")
# (find-idrisgitgrep "grep --color -nRH --null -e all-pdf *")
# (find-idrisgitgrep "grep --color -nRH --null -e documentation_complete *")
# (find-idrisgitgrep "grep --color -nRH --null -e reference *")
# (find-fline "~/usrc/Idris-dev/docs/reference/")
# (find-idrisgitfile "samples/")
# (find-idrisgitfile "samples/tutorial/")
;; (find-fline "~/usrc/Idris-dev/")
;; (find-pdf-page "~/usrc/Idris-dev/idris-tutorial.pdf")
;; (find-pdf-text "~/usrc/Idris-dev/idris-tutorial.pdf")
(code-pdf-page "idristut" "~/usrc/Idris-dev/idris-tutorial.pdf")
(code-pdf-text "idristut" "~/usrc/Idris-dev/idris-tutorial.pdf")
;; (find-idristutpage)
;; (find-idristuttext)
;; (find-pdf-page "~/usrc/Idris-dev/docs/_build/latex/idris-documentation-complete.pdf")
;; (find-pdf-text "~/usrc/Idris-dev/docs/_build/latex/idris-documentation-complete.pdf")
(code-pdf-page "idrisdocc" "~/usrc/Idris-dev/docs/_build/latex/idris-documentation-complete.pdf")
(code-pdf-text "idrisdocc" "~/usrc/Idris-dev/docs/_build/latex/idris-documentation-complete.pdf")
;; (find-idrisdoccpage)
;; (find-idrisdocctext)
# (find-idrisgitfile "docs/tutorial/typesfuns.rst" "``(2*)``")
#####
#
# idris-git-docs
# 2020dec23
#
#####
# «idris-git-docs» (to ".idris-git-docs")
* (eepitch-shell)
* (eepitch-kill)
* (eepitch-shell)
cd ~/usrc/Idris-dev/
git clean -dfx
git reset
# git pull
make user_doc_html |& tee omudh
make user_doc_pdf |& tee omudp
# (find-idrisgitfile "omudh")
# (find-idrisgitfile "omudp")
# (find-idrisgitfile "Makefile")
# (find-idrisgitfile "Makefile" "user_doc_html:")
# (find-idrisgitfile "Makefile" "user_doc_pdf:")
# (find-idrisgitfile "docs/_build/html/")
# (find-idrisgitfile "docs/_build/latex/")
# file:///home/edrx/usrc/Idris-dev/docs/_build/html/index.html
# file:///home/edrx/usrc/Idris-dev/docs/_build/html/reference/index.html
#####
#
# idris-mode
# 2019aug15
#
#####
# «idris-mode» (to ".idris-mode")
# «idris-mode-git» (to ".idris-mode-git")
# (find-epackage 'idris-mode)
# (find-elpafile "idris-mode-readme.txt")
# (code-c-d "idrismode" "~/.emacs.d/elpa/idris-mode-20200522.808/")
# (find-idrismodefile "")
# http://melpa.org/#/idris-mode
# https://github.com/idris-hackers/idris-mode
# http://davidchristiansen.dk/pubs/dtp2014-idris-mode.pdf
# http://docs.idris-lang.org/en/latest/reference/ide-protocol.html
# (find-idrismodegrep "grep --color -nH -e load *.el")
# (find-git-links "https://github.com/idris-hackers/idris-mode" "idrismodegit")
* (eepitch-shell)
* (eepitch-kill)
* (eepitch-shell)
rm -Rfv ~/usrc/idris-mode/
cd ~/usrc/
git clone https://github.com/idris-hackers/idris-mode
cd ~/usrc/idris-mode/
pdflatex documentation.tex
pdflatex documentation.tex
# (find-es "markdown" "pandoc")
# (find-man "1 pandoc")
#
pandoc readme.markdown -o readme.pdf
pandoc -s readme.markdown -o readme.html
# (find-idrismodegitfile "")
# (find-idrismodegitfile "documentation.tex")
# (find-idrismodegitfile "readme.markdown")
# (find-idrismodegitfile "readme.markdown" "C-c C-l")
# (find-idrismodegitfile "readme.markdown" "C-c C-t")
#####
#
# idris2-mode
# 2020aug06
#
#####
# «idris2-mode» (to ".idris2-mode")
# https://github.com/raders/idris2-mode
# (find-git-links "https://github.com/raders/idris2-mode" "idris2mode")
# (find-angg ".emacs" "idris2-mode")
* (eepitch-shell)
* (eepitch-kill)
* (eepitch-shell)
# rm -Rfv ~/usrc/idris2-mode/
cd ~/usrc/
git clone https://github.com/raders/idris2-mode
cd ~/usrc/idris2-mode/
# (code-c-d "idris2mode" "~/usrc/idris2-mode/")
# (find-idris2modefile "")
# (find-idris2modefile "README.md")
# (find-idris2modefile "idris2-mode.el")
(add-to-list 'load-path "~/usrc/idris2-mode/")
(autoload 'idris2-mode "idris2-mode" "Idris2 Mode." t)
(add-to-list 'auto-mode-alist '("\\.idr\\'" . idris2-mode))
# (find-evariable-links 'load-path)
# (find-epp load-path)
# (find-evariable-links 'auto-mode-alist)
# (find-epp auto-mode-alist)
# (find-efunctiondescr 'add-to-list)
#####
#
# idris-docs-online
# 2019nov10
#
#####
# «idris-docs-online» (to ".idris-docs-online")
# http://docs.idris-lang.org/en/latest/
# http://docs.idris-lang.org/en/latest/tutorial/index.html
# http://docs.idris-lang.org/en/latest/reference/index.html
# http://docs.idris-lang.org/en/latest/faq/faq.html
# http://docs.idris-lang.org/en/latest/proofs/index.html
#####
#
# idris-doc-complete
# 2019oct19
#
#####
# «idris-doc-complete» (to ".idris-doc-complete")
# (find-angg ".emacs" "idris")
# (find-idrisdoccpage)
# (find-idrisdocctext)
# (find-idrisdoccpage (+ 1 2) "1 The Idris Tutorial")
# (find-idrisdoccpage (+ 1 63) "2 Frequently Asked Questions")
# (find-idrisdoccpage (+ 1 68) "3 Implementing State-aware Systems in Idris: The ST Tutorial")
# (find-idrisdoccpage (+ 1 102) "4 The Effects Tutorial")
# (find-idrisdoccpage (+ 1 134) "5 Theorem Proving")
# (find-idrisdoccpage (+ 1 155) "6 Language Reference")
# (find-idrisdoccpage (+ 1 225) "7 Tutorials on the Idris Language")
# (find-idrisdoccpage (+ 1 2) "1 The Idris Tutorial")
# (find-idrisdoccpage (+ 1 4) "1.3 Types and Functions")
# (find-idrisdocctext (+ 1 4) "1.3 Types and Functions")
# (find-idrisdoccpage (+ 1 4) "1.3.1 Primitive Types")
# (find-idrisdocctext (+ 1 4) "1.3.1 Primitive Types")
# (find-idrisdoccpage (+ 1 5) "1.3.2 Data Types")
# (find-idrisdocctext (+ 1 5) "1.3.2 Data Types")
# (find-idrisdoccpage (+ 1 6) "1.3.3 Functions")
# (find-idrisdocctext (+ 1 6) "1.3.3 Functions")
# (find-idrisdoccpage (+ 1 7) "where clauses")
# (find-idrisdocctext (+ 1 7) "where clauses")
# (find-idrisdoccpage (+ 1 8) "Holes")
# (find-idrisdocctext (+ 1 8) "Holes")
# (find-idrisdoccpage (+ 1 8) "1.3.4 Dependent Types")
# (find-idrisdocctext (+ 1 8) "1.3.4 Dependent Types")
# (find-idrisdoccpage (+ 1 10) "Implicit Arguments")
# (find-idrisdocctext (+ 1 10) "Implicit Arguments")
# (find-idrisdoccpage (+ 1 11) "Note: Declaration Order and mutual blocks")
# (find-idrisdocctext (+ 1 11) "Note: Declaration Order and mutual blocks")
# (find-idrisdoccpage (+ 1 12) "1.3.5 I/O")
# (find-idrisdocctext (+ 1 12) "1.3.5 I/O")
# (find-idrisdoccpage (+ 1 12) "1.3.6 \"do\" notation")
# (find-idrisdocctext (+ 1 12) "1.3.6 \"do\" notation")
# (find-idrisdoccpage (+ 1 13) "1.3.7 Laziness")
# (find-idrisdocctext (+ 1 13) "1.3.7 Laziness")
# (find-idrisdoccpage (+ 1 13) "1.3.8 Codata Types")
# (find-idrisdocctext (+ 1 13) "1.3.8 Codata Types")
# (find-idrisdoccpage (+ 1 14) "1.3.9 Useful Data Types")
# (find-idrisdocctext (+ 1 14) "1.3.9 Useful Data Types")
# (find-idrisdoccpage (+ 1 15) "libs/base/Data/List.idr")
# (find-idrisdocctext (+ 1 15) "libs/base/Data/List.idr")
# (find-idrisdoccpage (+ 1 17) "Dependent Pairs")
# (find-idrisdocctext (+ 1 17) "Dependent Pairs")
# (find-idrisdoccpage (+ 1 17) "Records")
# (find-idrisdocctext (+ 1 17) "Records")
# (find-idrisdoccpage (+ 1 21) "1.4 Interfaces")
# (find-idrisdocctext (+ 1 21) "1.4 Interfaces")
# (find-idrisdoccpage (+ 1 22) "1.4.1 Default Definitions")
# (find-idrisdocctext (+ 1 22) "1.4.1 Default Definitions")
# (find-idrisdoccpage (+ 1 22) "1.4.2 Extending Interfaces")
# (find-idrisdocctext (+ 1 22) "1.4.2 Extending Interfaces")
# (find-idrisdoccpage (+ 1 23) "1.4.4 Monads and do-notation")
# (find-idrisdocctext (+ 1 23) "1.4.4 Monads and do-notation")
# (find-idrisdoccpage (+ 1 29) "1.5 Modules and Namespaces")
# (find-idrisdocctext (+ 1 29) "1.5 Modules and Namespaces")
# (find-idrisdoccpage (+ 1 40) "1.9 Theorem Proving")
# (find-idrisdocctext (+ 1 40) "1.9 Theorem Proving")
# (find-idrisdoccpage (+ 1 47) "sym : l = r -> r = l")
# (find-idrisdocctext (+ 1 47) "sym : l = r -> r = l")
#
# (find-idrisdoccpage (+ 1 63) "2 Frequently Asked Questions")
# (find-idrisdoccpage (+ 1 68) "3 Implementing State-aware Systems in Idris: The ST Tutorial")
# (find-idrisdoccpage (+ 1 102) "4 The Effects Tutorial")
# (find-idrisdoccpage (+ 1 134) "5 Theorem Proving")
#
# (find-idrisdoccpage (+ 1 155) "6 Language Reference")
# (find-idrisdocctext (+ 1 155) "6 Language Reference")
# (find-idrisdoccpage (+ 1 155) "SIX" "LANGUAGE REFERENCE")
# (find-idrisdocctext (+ 1 155) "SIX" "LANGUAGE REFERENCE")
# (find-idrisdoccpage (+ 1 157) "6.2.1 Comments")
# (find-idrisdocctext (+ 1 157) "6.2.1 Comments")
# (find-idrisdoccpage (+ 1 172) "Imports")
# (find-idrisdocctext (+ 1 172) "Imports")
# (find-idrisdoccpage (+ 1 173) "Records")
# (find-idrisdocctext (+ 1 173) "Records")
# (find-idrisdoccpage (+ 1 194) "6.11 DEPRECATED: Tactics and Theorem Proving")
# (find-idrisdocctext (+ 1 194) "6.11 DEPRECATED: Tactics and Theorem Proving")
# (find-idrisdoccpage (+ 1 225) "7 Tutorials on the Idris Language")
#####
#
# tutorial-samples
# 2019sep23
#
#####
# «tutorial-samples» (to ".tutorial-samples")
# (find-angg ".emacs" "idris")
# (find-idrisdoccpage)
# (find-idrisdocctext)
# (find-idrisgitfile "samples/tutorial/")
* (eepitch-idris)
* (eepitch-kill)
* (eepitch-idris)
even : Nat -> Bool
even Z = True
even (S k) = ?even_rhs
# (find-idrisdoccpage (+ 1 15) "libs/base/Data/List.idr")
# (find-idrisdocctext (+ 1 15) "libs/base/Data/List.idr")
# (find-sh "locate -i idris | grep -i prelude")
# (find-idrisgitfile "libs/prelude/")
# (find-idrisgitfile "libs/prelude/Prelude.idr")
# (find-idrisgitfile "libs/prelude/Prelude/")
# (find-idrisgitfile "libs/base/")
# (find-idrisgitfile "libs/base/Data/")
# (find-idrisgitfile "libs/base/Data/List.idr")
#####
#
# Juan Meleiro
# 2019sep22
#
#####
# «meleiro» (to ".meleiro")
# https://mail.google.com/mail/ca/u/0/#search/idr/FMfcgxwDqfDJzMgfbMkGJDlpbvsRzRJC
# (find-fline "~/IDRIS/Yoneda.idr")
# (find-fline "~/IDRIS/Representation.lidr")
# (find-sh "locate Category")
# (find-sh "locate Category | grep -i idris")
* (eepitch-shell)
* (eepitch-kill)
* (eepitch-shell)
w idris
cd ~/IDRIS/
idris Yoneda.idr
#####
#
# Nikolaj Kuntner's youtube channel about Idris
# 2019nov10
#
#####
# «nikolaj-kuntner» (to ".nikolaj-kuntner")
# https://github.com/Nikolaj-K/idris
# https://www.youtube.com/playlist?list=PL_vIhjXh1UTpfw8atiA31uP3F4Sjix_ZQ
#####
#
# "obj" vs. "obs cat1"
# 2019nov10
#
#####
# «obj-vs-obs-cat1» (to ".obj-vs-obs-cat1")
# (to "mailing-list")
# https://groups.google.com/forum/#!topic/idris-lang/NpDDeLNOeeU
# https://mail.google.com/mail/ca/u/0/#inbox/FMfcgxwDsFhxFfCkjJsmWbfFGdWhNSvf
# http://docs.idris-lang.org/en/latest/tutorial/typesfuns.html#records
# (find-idrisdoccpage (+ 1 17) "Records")
# (find-idrisdocctext (+ 1 17) "Records")
Question on "record" - "obj" vs. "obj cat1"
Hi list,
I'm a beginner with Idris, and I am trying to learn it by reading the
"Idris Tutorial" and the "Language Reference", and by reading the
documentation of idris-ct veeeery carefully and translating each
declaration and definition in idris-ct into type systems that I know -
so far it's been enough to me to use the strongest system of the
Barendregt Cube plus dependent sums of all kinds and an interpretation
of logic with equality...
I am having a problem with records, though. The definition of category
is this,
record Category where
constructor MkCategory
obj : Type
mor : obj -> obj -> Type
identity : (a : obj) -> mor a a
compose : (a, b, c : obj)
-> (f : mor a b)
-> (g : mor b c)
-> mor a c
leftIdentity : (a, b : obj)
-> (f : mor a b)
-> compose a a b (identity a) f = f
rightIdentity : (a, b : obj)
-> (f : mor a b)
-> compose a b b f (identity b) = f
associativity : (a, b, c, d : obj)
-> (f : mor a b)
-> (g : mor b c)
-> (h : mor c d)
-> compose a b d f (compose b c d g h) =
compose a c d (compose a b c f g) h
and then later we have this,
record CFunctor (cat1 : Category) (cat2 : Category) where
constructor MkCFunctor
mapObj : obj cat1 -> obj cat2
mapMor : (a, b : obj cat1)
-> mor cat1 a b
-> mor cat2 (mapObj a) (mapObj b)
preserveId : (a : obj cat1)
-> mapMor a a (identity cat1 a) = identity cat2 (mapObj a)
preserveCompose : (a, b, c : obj cat1)
-> (f : mor cat1 a b)
-> (g : mor cat1 b c)
-> mapMor a c (compose cat1 a b c f g)
= compose cat2 (mapObj a) (mapObj b) (mapObj c)
(mapMor a b f) (mapMor b c g)
and I am a bit confused about "obj" - it is used symply as "obj" in
"record Category", but in "record CFunctor" it is used as "obj cat1"
and "obj cat2", and I am not being able to translate these two
different uses into lower-level types and terms...
To be more precise: I know that each "obj" in "record Category" refers
to the field "obj" in the type "Category", and I know that each "obj"
in "record CFunctor" extracts the field "obj" of the category
following it, but I am not being able to find in the Language
Reference a detailed explanation of these two different uses of
"obj"... any hints on where I can find that?
Note: "not being able etc" means "I've spent some hours on the manuals
and with paper and pencil and whiteboards working out my ideas - but
certainly not time enough"! This is a _beginner_ question, I hope it's
ok to ask it here...
Thanks in advance =),
Eduardo Ochs
http://angg.twu.net/math-b.html
#####
#
# Understaning the definition of Pair
# 2019nov17
#
#####
# «Pair» (to ".Pair")
-- (find-idrisdoccpage (+ 1 136) "5.2.1 And (conjunction)")
-- (find-idrisdocctext (+ 1 136) "5.2.1 And (conjunction)")
-- (find-idrisdocctext (+ 1 136) "5.2.1 And (conjunction)" "Pair")
-- (find-idrisgitfile "libs/prelude/Builtins.idr" "data Pair :")
-- (find-idrisgitfile "libs/prelude/Builtins.idr" "%language UniquenessTypes")
-- (find-idrisgitfile "libs/prelude/Builtins.idr" "%language LinearTypes")
-- (find-idrisdoccpage (+ 1 173) "data Vect : Nat -> Type -> Type where")
-- (find-idrisdocctext (+ 1 173) "data Vect : Nat -> Type -> Type where")
-- (find-idrisdoccpage (+ 1 183) "ExplicitTypeDataRest" "::= ``where''")
-- (find-idrisdocctext (+ 1 183) "ExplicitTypeDataRest" "::= ``where''")
-- (find-idrisgitfile "libs/prelude/Prelude/Basics.idr" "fst")
-- (find-idrisgitfile "libs/prelude/Prelude/Basics.idr" "snd")
-- (find-idrisdoccpage (+ 1 181) "RigCount ::= ``1'' : ``0'' ;")
-- (find-idrisdocctext (+ 1 181) "RigCount ::= ``1'' : ``0'' ;")
data MyPair : (A : Type) -> (B : Type) -> Type where
-- MkPair : {A, B : Type} -> (1 a : A) -> (1 b : B) -> Pair A B
MyMkPair : {A, B : Type} -> ( a : A) -> ( b : B) -> MyPair A B
* (eepitch-to-buffer "*idris-repl*")
Pair 2 3 -- err
Pair Nat Nat
(2, 3)
fst (2, 3)
snd (2, 3)
#####
#
# Understanding "the"
# 2019nov17
#
#####
# «the» (to ".the")
-- (find-idrisdoccpage (+ 1 135) "5.2 Curry-Howard correspondence")
-- (find-idrisdocctext (+ 1 135) "5.2 Curry-Howard correspondence")
-- (find-idrisdoccpage (+ 1 135) "the (1=1) Refl")
-- (find-idrisdocctext (+ 1 135) "the (1=1) Refl")
-- (find-idrisgitgrep "grep --color -nrH -e the libs/")
-- (find-idrisgitgrep "grep --color -nrwH -e the libs/")
-- (find-idrisgitgrep "grep --color -nrwH -e the libs/ | grep -v '|'")
-- (find-idrisgitfile "libs/prelude/Prelude/Basics.idr" "the : (a : Type) -> (value : a) -> a")
#####
#
# idris-heyting-algebra
# 2019nov17
#
#####
# «idris-heyting-algebra» (to ".idris-heyting-algebra")
# https://github.com/Risto-Stevcev/idris-heyting-algebra
# https://github.com/Risto-Stevcev/idris-heyting-algebra/issues/2
# https://github.com/Risto-Stevcev/idris-heyting-algebra/issues/2#issuecomment-554748819 my comment
# https://libraries.io/bower/
# https://libraries.io/bower/idris-heyting-algebra
# bower install idris-heyting-algebra
# (find-es "javascript" "bower")
# (find-git-links "https://github.com/Risto-Stevcev/idris-heyting-algebra" "idrisha")
* (eepitch-shell)
* (eepitch-kill)
* (eepitch-shell)
rm -Rfv ~/usrc/idris-heyting-algebra/
cd ~/usrc/
git clone https://github.com/Risto-Stevcev/idris-heyting-algebra
cd ~/usrc/idris-heyting-algebra/
git branch --list -a
git for-each-ref
PAGER=cat git log --oneline --graph --all -20
# (find-fline "~/usrc/")
# (find-fline "~/usrc/idris-heyting-algebra/")
# (find-gitk "~/usrc/idris-heyting-algebra/")
# (code-c-d "idrisha" "~/usrc/idris-heyting-algebra/")
# (find-idrishafile "")
# (find-idrishafile "Interfaces/HeytingAlgebra.idr")
# (find-idrishafile "heyting-algebra.ipkg")
cd ~/usrc/idris-heyting-algebra/
time nice \
idris --V2 --install heyting-algebra.ipkg |& tee oiiha
# Broken.
#####
#
# import
# 2019nov17
#
#####
# «import» (to ".import")
-- (find-idrisdoccpage (+ 1 172) "Imports")
-- (find-idrisdocctext (+ 1 172) "Imports")
-- (find-idrisdoccpage (+ 1 177) "Import" "::=")
-- (find-idrisdocctext (+ 1 177) "Import" "::=")
-- (find-idrisgitfile "libs/base/Data/Vect.idr" "data Vect :")
import public Data.Vect
{-
* (eepitch-to-buffer "*idris-repl*")
-}
#####
#
# preorders
# 2019nov19
#
#####
# «preorders» (to ".preorders")
# (find-idrisgitsh "find * | sort")
# (find-idrisgitfile "libs/base/Syntax/PreorderReasoning.idr")
# (find-idrisgitfile "libs/contrib/Decidable/Order.idr")
# (find-idrisgitfile "libs/contrib/Decidable/Order.idr" "interface Preorder")
# (find-idrisgitgrep "grep --color -nriH -e preorder libs/")
# (find-idrisgitfile "libs/contrib/Control/Algebra/Lattice.idr")
#####
#
# Either
# 2019nov19
#
#####
# «Either» (to ".Either")
# (find-idrisdoccpage (+ 1 136) "5.2.2 Or (disjunction)")
# (find-idrisdocctext (+ 1 136) "5.2.2 Or (disjunction)")
# (find-idrisdocctext (+ 1 136) "5.2.2 Or (disjunction)" "Either")
# (find-idrisgitgrep "grep --color -nriH -e preorder libs/")
# (find-idrisgitfile "libs/prelude/Prelude/Either.idr")
#####
#
# lowercase
# 2019nov20
#
#####
# «lowercase» (to ".lowercase")
# (find-idrisdoccpage (+ 1 10) "lower case")
# (find-idrisdocctext (+ 1 10) "lower case")
# (find-idrisdoccpage (+ 1 11) "lowercase")
# (find-idrisdocctext (+ 1 11) "lowercase")
# (find-idrisdoccpage (+ 1 65) "lower case")
# (find-idrisdocctext (+ 1 65) "lower case")
# (find-idrisdoccpage (+ 1 65) "lower case")
# (find-idrisdocctext (+ 1 65) "lower case")
# (find-idrisdoccpage (+ 1 209) "lower case")
# (find-idrisdocctext (+ 1 209) "lower case")
# (find-bradytdpage (+ 1 37) "lowercase letter")
# (find-bradytdtext (+ 1 37) "lowercase letter")
# (find-idrisdoccpage (+ 1 30) "top level")
# (find-idrisdocctext (+ 1 30) "top level")
# (find-idrisdoccpage (+ 1 52) "top level")
# (find-idrisdocctext (+ 1 52) "top level")
# (find-idrisdoccpage (+ 1 141) "top level")
# (find-idrisdocctext (+ 1 141) "top level")
#####
#
# Generating bytecode
# 2019dec04
#
#####
# «bytecode» (to ".bytecode")
# (find-idrisdoccpage (+ 1 4) "bytecode version of the file")
# (find-idrisdocctext (+ 1 4) "bytecode version of the file")
* (eepitch-shell)
* (eepitch-kill)
* (eepitch-shell)
cd ~/IDRIS/
idris HAJ.idr
:?
:q
laf HAJ*
# (find-angg "IDRIS/HAJ.idr")
#####
#
# Command line options
# 2019dec13
#
#####
# «command-line» (to ".command-line")
# (find-man "idris")
# (find-man "idris" "-c,--compileonly")
# (find-idrisgitgrep "grep --color -nirH --null -e command")
# (find-idrisgitgrep "grep --color -nirH --null -e 'command line'")
# (find-idrisgitgrep "grep --color -nirH --null -e '-o'")
# (find-idrisgitgrep "grep --color -nirH --null -e '--warnpartial'")
# (find-idrisgitgrep "grep --color -nirH --null -e 'warnpartial'")
# (find-idrisgitfile "src/Idris/CmdOptions.hs" "\"warnpartial\"")
# (find-idrisgitfile "test/pkg010/expected" "[-o|--output FILE]")
#####
#
# holes
# 2019dec19
#
#####
# «holes» (to ".holes")
# (find-books "__comp/__comp.el" "brady")
# (find-bradytddpage (+ 26 20) "1.4.4 Incomplete definitions: working with holes")
# (find-bradytddtext (+ 26 20) "1.4.4 Incomplete definitions: working with holes")
# (find-idrisdoccpage (+ 1 8) "Holes")
# (find-idrisdocctext (+ 1 8) "Holes")
# (find-idrisdoccpage (+ 1 99) "using holes")
# (find-idrisdocctext (+ 1 99) "using holes")
# (find-idrisdoccpage (+ 1 145) "All holes have now been solved.")
# (find-idrisdocctext (+ 1 145) "All holes have now been solved.")
#####
#
# indentation
# 2020feb22
#
#####
# «indentation» (to ".indentation")
# (find-idrisdoccpage)
# (find-idrisdocctext)
# (find-idrisdoccpage (+ 1 5) "New declarations must begin at the same")
# (find-idrisdocctext (+ 1 5) "New declarations must begin at the same")
# (find-idrisdoccpage (+ 1 7) "must be indented further than the outer")
# (find-idrisdocctext (+ 1 7) "must be indented further than the outer")
# (find-idrisdoccpage (+ 1 13) "must begin in the same column")
# (find-idrisdocctext (+ 1 13) "must begin in the same column")
# (find-bradytddpage (+ 26 46) "2.4.1 Whitespace significance: the layout rule")
# (find-bradytddtext (+ 26 46) "2.4.1 Whitespace significance: the layout rule")
#####
#
# Brady's book: examples
# 2020feb21
#
#####
# «bradys-book-examples» (to ".bradys-book-examples")
# «bradytdd» (to ".bradytdd")
# (find-books "__comp/__comp.el" "brady")
# (find-angg ".emacs" "idris-bradytdd")
# (find-bradytddpage 23 "https://github.com/edwinb/")
# (find-bradytddtext 23 "https://github.com/edwinb/")
# https://github.com/edwinb/TypeDD-Samples
* (eepitch-shell)
* (eepitch-kill)
* (eepitch-shell)
# rm -Rfv ~/usrc/TypeDD-Samples/
cd ~/usrc/
git clone https://github.com/edwinb/TypeDD-Samples
cd ~/usrc/TypeDD-Samples/
export PAGER=cat
git branch --list -a
git for-each-ref
git log --oneline --graph --all -20
# (find-fline "~/usrc/")
# (find-fline "~/usrc/TypeDD-Samples/")
# (find-gitk "~/usrc/TypeDD-Samples/")
# (code-c-d "bradytdd" "~/usrc/TypeDD-Samples/")
# (find-bradytddfile "")
# (find-bradytddsh "find * | sort")
# (find-bradytddsh "find * | sort -n")
cd ~/usrc/TypeDD-Samples/
#####
#
# postulate
# 2020apr25
#
#####
# «postulate» (to ".postulate")
# https://stackoverflow.com/questions/27999552/postulates-in-idris
#####
#
# snap install idris2
# 2020apr27
#
#####
# «snap-install-idris2» (to ".snap-install-idris2")
# (find-es "snap")
* (eepitch-shell)
* (eepitch-kill)
* (eepitch-shell)
snap install idris2
snap info idris2
snap help install
snap install --edge idris2
snap install --edge --classic idris2
#####
#
# idris2
# 2020may25 / 2020dec22
#
#####
# «idris2» (to ".idris2")
# (find-es "scheme" "chez-scheme")
# https://www.idris-lang.org/idris-2-version-020-released.html
# https://www.idris-lang.org/idris-2-version-021-released.html
# https://www.idris-lang.org/pages/download.html
# https://www.idris-lang.org/idris2-src/idris2-latest.tgz
# (find-fline "$S/https/www.idris-lang.org/idris2-src/")
# (find-fline "$S/https/www.idris-lang.org/idris2-src/idris2-latest.tgz")
#
# (code-c-d "idris2" "~/usrc/Idris2-0.2.1/")
# (find-idris2file "")
# (find-idris2file "README.md")
# (find-idris2file "README.md" "make bootstrap SCHEME=chez")
* (eepitch-shell)
* (eepitch-kill)
* (eepitch-shell)
# (find-fline "~/usrc/Idris2-0.2.1/")
rm -Rv ~/usrc/Idris2-0.2.1/
mkdir ~/usrc/Idris2-0.2.1/
tar -C ~/usrc/ -xvzf $S/https/www.idris-lang.org/idris2-src/idris2-latest.tgz
cd ~/usrc/Idris2-0.2.1/
* (eepitch-shell2)
* (eepitch-kill)
* (eepitch-shell2)
cd ~/usrc/Idris2-0.2.1/
make bootstrap SCHEME=chez |& tee omb
make install |& tee omi
idris2
:q
# (find-idris2sh "find * | sort")
# (find-idris2file "bootstrap/idris2_app/idris2.ss")
# (find-idris2file "src/Core/")
# (find-idris2file "omb")
# (find-idris2file "omi")
# (find-fline "~/.idris2/")
# (find-fline "~/.idris2/bin/idris2")
* (eepitch-shell)
* (eepitch-kill)
* (eepitch-shell)
cd ~/usrc/Idris2-0.2.1/
cd docs
make html |& tee omhtml
make latexpdf |& tee omlatexpdf
# (find-idris2file "docs/omlatexpdf")
# (find-idris2file "docs/")
~/.idris2/bin/idris2
* (eepitch-shell)
* (eepitch-kill)
* (eepitch-shell)
# (find-fline "~/bin/idris2")
idris2
#####
#
# idris2-docs
# 2020sep10
#
#####
# «idris2-docs» (to ".idris2-docs")
# https://idris2.readthedocs.io/en/latest/typedd/typedd.html
<edrx> hi - newbie question:
<edrx> I'm on Debian, and when I was using Idris 1 I generated the
docs by cloning http://github.com/idris-lang/Idris-dev into
~/usrc/Idris-dev/, and then running make user_doc_pdf... I
would then get a PDF in
~/usrc/Idris-dev/docs/_build/latex/idris-documentation-complete.pdf
with "everything", for some value of "everything"...
<jfdm> i think we curtail the PDF output to just the tutorial
<edrx> is there something similar for Idris2? some examples from
Brady's book seem to need changed to run in idris2...
<jfdm> it's a result of the limitation of Readthedocs only
producing a single pdf
<jfdm> idris2.readthedocs.io
<edrx> excellent! thanks! =)
<jfdm> https://idris2.readthedocs.io/en/latest/typedd/typedd.html
<jfdm> there is also idris.readthedocs.io for idris1
<jfdm> docs.idris-lang.org redirects to the latter
<jfdm> at somepoint it will redirect to Idris2
https://idris2.readthedocs.io/en/latest/typedd/typedd.html
#####
#
# idris2-git
# 2020sep10
#
#####
# «idris2-git» (to ".idris2-git")
# (find-angg ".emacs" "idris2-tutorial")
# https://github.com/idris-lang/Idris2/blob/master/docs/source/index.rst
# (find-git-links "https://github.com/idris-lang/Idris2" "idris2git")
# https://github.com/idris-lang/Idris2
* (eepitch-shell)
* (eepitch-kill)
* (eepitch-shell)
# rm -Rfv ~/usrc/Idris2/
cd ~/usrc/
git clone https://github.com/idris-lang/Idris2
cd ~/usrc/Idris2/
git clean -dfx
git reset --hard
# git pull
export PAGER=cat
git branch --list -a
git for-each-ref
git log --oneline --graph --all -20
cd ~/usrc/Idris2/
cd docs
make html |& tee omhtml
make latexpdf |& tee omlatexpdf
# (find-fline "~/usrc/")
# (find-fline "~/usrc/Idris2/")
# (find-gitk "~/usrc/Idris2/")
# (code-c-d "idris2git" "~/usrc/Idris2/")
# (find-idris2gitfile "")
# (find-idris2gitfile "INSTALL.md")
# (find-idris2gitfile "Makefile")
# (find-idris2gitfile "docs/")
# (find-idris2gitfile "docs/README.md" "## Build Instructions")
# (find-idris2gitfile "docs/README.md" "pip install sphinx_rtd_theme")
# (find-idris2gitfile "docs/Makefile")
# (find-idris2gitfile "docs/build/html/")
# (find-idris2gitfile "docs/build/latex/")
# file:///home/edrx/usrc/Idris2/docs/build/html/index.html
# file:///home/edrx/usrc/Idris2/docs/build/html/reference/index.html
# (code-pdf-page "idris2tut" "~/usrc/Idris2/docs/build/latex/idris-tutorial.pdf")
# (code-pdf-text "idris2tut" "~/usrc/Idris2/docs/build/latex/idris-tutorial.pdf")
# (find-idris2tutpage)
# (find-idris2tuttext)
# https://idris2.readthedocs.io/_/downloads/en/latest/pdf/
# (find-fline "~/LOGS/2020sep10.idris")
#####
#
# learn-idris.net
# 2020jun06
#
#####
# «learn-idris.net» (to ".learn-idris.net")
# https://learn-idris.net/
#####
#
# jake-gillberg
# 2020jun24
#
#####
# «jake-gillberg» (to ".jake-gillberg")
# https://github.com/Jake-Gillberg/idris-ct
#####
#
# preorder-reasoning
# 2020dec23
#
#####
# «preorder-reasoning» (to ".preorder-reasoning")
# http://docs.idris-lang.org/en/latest/reference/misc.html#preorder-reasoning
# http://docs.idris-lang.org/en/latest/tutorial/syntax.html
# http://docs.idris-lang.org/en/latest/tutorial/typesfuns.html#data-types
# (find-idrisgitfile "libs/base/Syntax/PreorderReasoning.idr")
# (find-idris2file "libs/contrib/Syntax/PreorderReasoning.idr")
# (find-fline "~/LOGS/2020dec22.idris")
# (find-idris2sh "find * | sort")
# (find-idris2sh "find * | sort | grep Syntax")
# (find-idris2sh "find * | sort | grep 'idr$'")
# (find-idris2sh "grep '={' $(find * | sort | grep 'idr$')")
# (find-idris2sh "grep 'Preor' $(find * | sort | grep 'idr$')")
# (find-idris2grep "grep --color -nRH --null -e 'Preorder reasoning' *")
# (find-idris2grep "grep --color -nRH --null -e '={' $(find * | sort | grep rst)")
# (find-idris2grep "grep --color -nRH --null -e '={' $(find * | sort | grep 'idr$')")
#####
#
# Eckart Hertzler's tutorial
# 2020dec26
#
#####
# «eckart» (to ".eckart")
# https://github.com/eckart
# https://github.com/eckart/gl-idris
# https://github.com/eckart/idris-tutorial
# http://eckart.github.io/programming/graphics/idris/2015/09/13/hello-world.html
* (eepitch-shell)
* (eepitch-kill)
* (eepitch-shell)
# rm -Rfv ~/usrc/gl-idris/
cd ~/usrc/
git clone https://github.com/eckart/gl-idris
cd ~/usrc/gl-idris/
export PAGER=cat
git branch --list -a
git for-each-ref
git log --oneline --graph --all -20
# (code-c-d "glidris" "~/usrc/gl-idris/")
# (find-glidrisfile "")
* (eepitch-shell)
* (eepitch-kill)
* (eepitch-shell)
# rm -Rfv ~/usrc/idris-tutorial/
cd ~/usrc/
git clone https://github.com/eckart/idris-tutorial
cd ~/usrc/idris-tutorial/
export PAGER=cat
git branch --list -a
git for-each-ref
git log --oneline --graph --all -20
# (find-fline "~/usrc/")
# (find-fline "~/usrc/idris-tutorial/")
# (find-gitk "~/usrc/idris-tutorial/")
# (code-c-d "idristutorial" "~/usrc/idris-tutorial/")
# (find-idristutorialfile "")
#####
#
# juan-HAJ-dec-2020
# 2020dec22
#
#####
# «juan-HAJ-dec-2020» (to ".juan-HAJ-dec-2020")
# (find-fline "/tmp/HAJ-2020-12-22-23-30.idr")
* (eepitch-shell)
* (eepitch-kill)
* (eepitch-shell)
idris2
:doc replace
-- See the documentation on Preorder Reasoning [1] for the meaning of
-- the following syntax. For that, we need to define a `step` and `qed`
-- functions -- just aliases for transitivity and reflexivity.
-- [1]: http://docs.idris-lang.org/en/latest/reference/misc.html#preorder-reasoning
step : {h : HAJ} -> (x : o_H h) -> le h x y -> le h y z -> le h x z
step {h} x = trans h
qed : {h : HAJ} -> (x : o_H h) -> le h x x
qed {h} x = refl h x
Mop : {h : HAJ} -> {p, q : o_H h} -> (le h) (o_J h ((and h) p q)) (o_J h q)
Mop {h} {p} {q} = (o_J h ((and h) p q)) ={ replace (sym $ o_J3 h) (refl h (o_J h ((and h) p q))) }=
-- ^^^^^^^^^ 1 ^^^^^^^^^^ ^^^^^^^^^^^^^^ 2 ^^^^^^^^^^^^^
-- 1: replace (p & q)* by (p* & q*) in the second term of the inequality
-- 2: (p & q)* <= (p & q)* to obtain
-- (p & q)* <= (p* & q*)
(and h (o_J h p) (o_J h q)) ={ ande2 h (refl h (and h (o_J h p) (o_J h q))) }=
-- ^^ 1 ^^ ^^^^^^^^^^^^^^^ 2 ^^^^^^^^^^^^^^^^
-- 1: eliminate first term on the right-hand side of the inequality
-- 2: (p* & q*) <= (p* & q*)
-- to obtain (p* & q*) <= q*
(o_J h q) QED -- because we wanted (p & q)* <= q*
-- (find-idrisgitfile "libs/prelude/Prelude/Basics.idr" "cong :")
https://www.tumblr.com/tagged/ivor-the-engine
https://en.wikipedia.org/wiki/Ivor_the_Engine#Idris_the_Dragon
https://edwinb.wordpress.com/2013/10/28/interactive-idris-editing-with-vim/
http://docs.idris-lang.org/en/latest/faq/faq.html#will-there-be-support-for-unicode-characters-for-operators
https://en.wikipedia.org/wiki/Cadair_Idris
https://docs.haskellstack.org/en/stable/travis_ci/
I usually use nix to develop with Idris:
$ idris --version
bash: idris: command not found
$ nix-shell -p idris
[nix-shell:~]$ idris --version
1.3.2
[nix-shell:~]$ exit
That works exactly the same on here Arch, NixOS, and Debian, so it
should work fine on Ubuntu too.
--
Anthony Carrico
(2020jan19)
https://ice1000.org/2019/06-20-SolveMeta Type inference under dependent type (meta variables)
https://hypefortypes.github.io/
https://hypefortypes.github.io/stuff/01/intro-20200114.pdf
https://eb.host.cs.st-andrews.ac.uk/Idris/exercises.pdf
http://docs.idris-lang.org/en/latest/faq/faq.html
https://idris2.readthedocs.io/en/latest/updates/updates.html
https://github.com/idris-community/idris2-elab-util
https://github.com/idris-community/idris2-elab-util/blob/main/src/Doc/Index.md
https://whatisrt.github.io/dependent-types/2020/02/18/agda-vs-coq-vs-idris.html
https://mail.google.com/mail/ca/u/0/#inbox/FMfcgzGkXSRLngZQHdCCBwtjFZFLvDPB [Idris] Why Idris don't have guards?
# Local Variables:
# coding: utf-8-unix
# ee-anchor-format: "«%s»"
# End: