|
Warning: this is an htmlized version!
The original is across this link, and the conversion rules are here. |
#######
#
# E-scripts on programs to typeset deduction trees.
#
# 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.
#
# 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/dednat.e>
# or at <http://angg.twu.net/e/dednat.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/>.
#
#######
# «.dednat.lua» (to "dednat.lua")
# «.dednat.icn» (to "dednat.icn")
# «.dednat4-tgz-tests» (to "dednat4-tgz-tests")
# «.thereplusxy» (to "thereplusxy")
# «.splitdist» (to "splitdist")
# «.phantom-nodes» (to "phantom-nodes")
# «.tex-src-tgz» (to "tex-src-tgz")
# «.eepitch-dednat4» (to "eepitch-dednat4")
# «.dednat4-test» (to "dednat4-test")
# «.dednat41-test» (to "dednat41-test")
# «.dednat4-demo1» (to "dednat4-demo1")
# «.dednat41-demo1» (to "dednat41-demo1")
# «.tgz:make-demo1» (to "tgz:make-demo1")
# «.visible-phantoms» (to "visible-phantoms")
# «.dednat4.el» (to "dednat4.el")
# «.symlinks» (to "symlinks")
# «.dednat4-log» (to "dednat4-log")
# «.2008filterp-texsrc» (to "2008filterp-texsrc")
# «.lpeg» (to "lpeg")
#####
#
# dednat.lua (obsolete)
# 2001may15
#
#####
# «dednat.lua» (to ".dednat.lua")
# (find-angg "LUA/dednat.lua")
# (find-angg "LATEX/Makefile")
# (find-angg "LATEX/Makefile" "dednat.lua")
# (find-angg "LATEX/Makefile" "dn_to_dnt")
#*
# (find-angg "LATEX/tese2.sty")
# (find-angg "LATEX/proof.edrx.sty")
cd ~/LATEX/
rm -v tmp.dn tmp.dnt
cat > tmp.tex <<'%%%'
% \input tese2.sty
\documentclass{book}
\usepackage{proof.edrx}
\def\ded#1{\csname ded-#1\endcsname}
\def\defded#1#2{\expandafter\def\csname ded-#1\endcsname{#2}}
\input tmp.dnt
\begin{document}
%
%:*->*\to *
%:
%: a [a->b]^1
%: -----------
%: b
%: ---------1
%: (a->b)->b
%:
%: ^dedtest
%:
$$\ded{dedtest}$$
%
\end{document}
%%%
make tmp.dvi
rexdvi tmp.dvi
#*
#####
#
# dednat.icn (obsolete)
# 2001may15
#
#####
# «dednat.icn» (to ".dednat.icn")
# (find-angg "LATEX/dednat.icn")
#####
#
# dednat4: tgz and tests
# 2008may26
#
#####
# «dednat4-tgz-tests» (to ".dednat4-tgz-tests")
# (find-es "xypic")
# (find-es "xypic" "dednat41-test")
# (find-es "xypic" "dednat41-demo1")
# (find-es "xypic" "eepitch-dednat4")
# (find-angg ".emacs" "eepitch-dednat4")
# (find-angg ".emacs" "dednat4")
# (find-angg ".emacs" "eedn4a")
# (find-dn4 "")
# (find-dn4 "Makefile")
# The README is crap:
# (find-dn4file "README")
# This is ok - copy to the dednat4/ dir:
# (find-THLw3m "dednat4.html")
# (find-TH "dednat4")
# (find-sh "grep IMG ~/TH/dednat4.blogme")
# It needs a hacker's guide, though... get logs from:
# (find-es "xypic" "eepitch-dednat4")
# Add: at: x y tag
# .xy+= x y
# there+: x y tag
# (find-anggfile "IMAGES/Atimes-dnt.png")
# (find-anggfile "IMAGES/Atimes.png")
# (find-anggfile "IMAGES/TfromFtoG.png")
# (find-anggfile "IMAGES/eqfib-trans.png")
# (find-anggfile "IMAGES/lccc-bcc.png")
# (find-anggfile "IMAGES/lccc-frob.png")
# (find-anggfile "IMAGES/preslim.png")
# (find-zsh "
cd ~/IMAGES/
A=(
Atimes-dnt.png
Atimes.png
TfromFtoG.png
eqfib-trans.png
lccc-bcc.png
lccc-frob.png
preslim.png
)
laf $A
")
#####
#
# there+xy:
# 2008jun01
#
#####
# «thereplusxy» (to ".thereplusxy")
# (find-LATEXfile "2008sheaves.tex" "thereplusxy =")
#####
#
# understand harrownodes and varrownodes
# 2008jun02
#
#####
# «splitdist» (to ".splitdist")
# (find-dn4 "dednat41.lua")
# (find-dn4 "experimental.lua")
Suppose that we want to draw a diagram like this one:
A |-----> FA
| -
| |-> |
v v
B |-----> FB
* (eepitch-dednat4)
* (eepitch-kill)
* (eepitch-dednat4)
require "experimental"
= splitdist(100, 200, nil, 20, nil)
--> 140 160
#####
#
# Documentation about phantom nodes
# 2008jun24
#
#####
# «phantom-nodes» (to ".phantom-nodes")
# Moved to: (find-dn4 "README.phantoms")
#####
#
# LaTeX source tarballs for my .texs
# 2008jun08
#
#####
# «tex-src-tgz» (to ".tex-src-tgz")
* (eepitch-shell)
* (eepitch-kill)
* (eepitch-shell)
rm -Rv /tmp/te/
mkdir /tmp/te/
cd /tmp/te/
# (find-fline "~/LATEX/2008bcc.tex")
F=$HOME/LATEX/2008bcc.tex
cp -av $F .
cp -av ~/dednat4/examples/edrx08.sty .
cp -av ~/dednat4/examples/edrxdnt.tex .
cp -av ~/dednat4/examples/edrxdefs.tex .
cp -av ~/dednat4/examples/edrxheadfoot.tex .
~/dednat4/dednat41 $(basename $F)
cp -av $S/http/www.ctan.org/tex-archive/macros/latex/contrib/lkproof/proof.sty .
unzip -o $S/ftp/ftp.math.mcgill.ca/pub/barr/diagxy.zip diagxy.tex
latex $(basename $F)
# (find-fline "/tmp/te/")
# (find-dn4exfile "")
# (find-dn4file "Makefile")
# (find-dn4file "Makefile" "TATPROOFSFILE =")
# (find-dn4file "Makefile" "DIAGXYFILE")
# Add this?
# (find-dn4file "dednat41.lua")
# Generated by dednat41.lua
#####
#
# eepitch-dednat4
# 2008may11
#
#####
# «eepitch-dednat4» (to ".eepitch-dednat4")
# (find-angg ".emacs" "eepitch-dednat4")
# (find-angg "LUA/lua50init.lua" "load_dednat4")
# (find-dn4 "dednat41.lua")
# (find-dn4 "dednat41.lua" "tree-lib" "dolinenumbers")
* (eepitch-dednat4)
* (eepitch-kill)
* (eepitch-dednat4)
PP(abbrevs)
process "/home/edrx/dednat4/examples/edrx08.sty"
PP(abbrevs)
PP(heads)
* (eepitch-dednat4)
* (eepitch-kill)
* (eepitch-dednat4)
dolinenumbers = nil
diagram "miniadj"
dxy2Dx " 100 140 "
dxy2D " 140 a^L <= a "
dxy2D " - - "
dxy2D " | | "
dxy2D " v v "
dxy2D " 100 b => b^R "
PP("nodes =", nodes)
pushtag "a^L"; pushtag "a"; dof "<="
pushtag "a^L"; pushtag "b"; dof "|->"
pushtag "a"; pushtag "b^R"; dof "|->"
pushtag "b"; pushtag "b^R"; dof "=>"
PP("arrows =", arrows)
enddiagram()
* (eepitch-dednat4)
* (eepitch-kill)
* (eepitch-dednat4)
dolinenumbers = nil
mytostringk = mytostringk2
dofs "diagram miniadj2"
dofs "2Dx 100 140 "
dofs "2D 140 a^L <= a "
dofs "2D - - "
dofs "2D | | "
dofs "2D v v "
dofs "2D 100 b => b^R "
dofs "(( a^L a <= a^L b |-> a b^R |->"
printf("xs = %s\n", mytostring(xs))
for i=1,#nodes do printf("nodes[%d] = %s\n", i, mytostring(nodes[i])) end
for i=1,#arrows do printf("arrows[%d] = %s\n", i, mytostring(arrows[i])) end
for i=1,#ds do printf("ds[%d] = %s\n", i, mytostring(ds[i])) end
for i=1,#depths do printf("depths[%d] = %s\n", i, mytostring(depths[i])) end
PP(keys(nodes))
dofs " b b^R => ))"
dofs "enddiagram"
Note: due to a bad design decision the elements of ds are "in the
wrong order" - to push a new element we move the old elements from the
positions 1..n to 2..n+1, and then we set ds[1] to the new element...
this simplifies accessing the elements at the top of the stack, but
complicates all the rest - especially "@" and operations with the
array "depths".
One possible fix (dirty trick): use a metatable with a "__call" entry
for the table "ds"; make ds(2) return ds[-2] for any value of 2.
Notes (obsolete):
%L at = function (index) return ds[#ds - depths[1] - index] end
%L PP("@ 0 =", at(0))
%L PP("@ 1 =", at(1))
%L PP("@ 2 =", at(2))
%L PP(ds[#ds])
%L PP(ds[#ds - 1])
%L PP(#ds)
%L PP(ds)
%L mytostringk = mytostringk2
%L printf("xs = %s\n", mytostring(xs))
%L for i=1,#nodes do printf("nodes[%d] = %s\n", i, mytostring(nodes[i])) end
%L for i=1,#arrows do printf("arrows[%d] = %s\n", i, mytostring(arrows[i])) end
%L for i=1,#ds do printf("ds[%d] = %s\n", i, mytostring(ds[i])) end
%L for i=1,#depths do printf("depths[%d] = %s\n", i, mytostring(depths[i])) end
%L PP(keys(nodes))
% (find-sh "cd ~/LATEX/ && lua51 ~/dednat4/dednat41.lua tmp.tex")
% (find-angg "LUA/lua50init.lua")
#####
#
# Testing dednat41
# 2008may19
#
#####
# «dednat4-test» (to ".dednat4-test")
# «dednat41-test» (to ".dednat41-test")
# (find-dn4 "Makefile")
# (find-node "(kpathsea)File lookup")
# (find-dn4exfile "dednat4.el")
# (find-eevtmpfile "")
# (find-eevtmpfile "ee.sh")
# (find-LATEXfile "" "tmp.tex")
# (find-LATEXfile "tmp.tex")
# (find-LATEXfile "ee.tex")
# (find-angg ".emacs")
# (find-angg ".emacs" "dednat4")
# (find-es "xypic" "eepitch-dednat4")
# (find-angg ".emacs" "eedn4a")
* (eepitch-shell)
* (eepitch-kill)
* (eepitch-shell)
rm -Rv /tmp/dntest/
mkdir /tmp/dntest/
cd /tmp/dntest/
cd ~/dednat4/
make S=$S TEXDIR=/tmp/dntest texfiles
cd /tmp/dntest/
DN4EXDIR=$HOME/dednat4/examples/
cp -v $DN4EXDIR/edrxmain41a.tex tmp.tex
cp -v $DN4EXDIR/eedemo1.tex ee.tex
cp -v $DN4EXDIR/edrx08.sty edrx08.sty
~/dednat4/dednat41 tmp.tex
TEXINPUTS=$DN4EXDIR: latex tmp.tex
# (find-fline "/tmp/dntest/")
# (find-fline "/tmp/dntest/tmp.tex")
# (find-dvipage "/tmp/dntest/tmp.dvi")
# «dednat4-demo1» (to ".dednat4-demo1")
# «dednat41-demo1» (to ".dednat41-demo1")
# (find-dn4 "Makefile" "demo1")
* (eepitch-shell)
* (eepitch-kill)
* (eepitch-shell)
cd ~/dednat4/
rm -Rv demos/
mkdir demos/
make demo1
# (find-dn4 "demos/")
# (find-man "unzip")
#####
#
# dednat4: "make demo1" (from the tarball)
# 2008jun25
#
#####
# «tgz:make-demo1» (to ".tgz:make-demo1")
* (eepitch-shell)
* (eepitch-kill)
* (eepitch-shell)
rm -Rv /tmp/dn4t/
mkdir /tmp/dn4t/
cd /tmp/dn4t/
tar -xvzf ~/dednat4/dednat4.tgz
make S=$S demo1 |& tee om
# (find-fline "/tmp/dn4t/")
#####
#
# visible phantoms
# 2008jun27
#
#####
# «visible-phantoms» (to ".visible-phantoms")
# (find-fline "~/tmp/phantom-nodes.png")
%*
% (eedn4a-bounded)
%L phantomnode = "\\myphantom{O}"
\def\myphantom{\phantom}
%D diagram harrowdemo
%D 2Dx 100 +30
%D 2D 100 A |-----> FA
%D 2D | -
%D 2D f | |-> | Ff
%D 2D v v
%D 2D +30 B |-----> FB
%D 2D
%D (( A FA |->
%D A B -> .plabel= l f
%D FA FB -> .plabel= r Ff
%D B FB |->
%D A FB harrownodes nil 20 nil |->
%D ))
%D enddiagram
%D
$$\diag{harrowdemo}
\qquad
{\def\myphantom{\red}
\diag{harrowdemo}
}
$$
%*
#####
#
# dednat4.el
# 2008jun27
#
#####
# «dednat4.el» (to ".dednat4.el")
# (find-dn4 "dednat4.el")
* (eepitch-shell)
* (eepitch-kill)
* (eepitch-shell)
cd ~/dednat4/
lua51 -e 'dofile"dednat41.lua"' -i
require "experimental"
#####
#
# symlinks: tmp.tex -> edrxmain41.tex and ee.tex -> eedemo1.tex
# 2008jun27
#
#####
# «symlinks» (to ".symlinks")
# (find-dn4file "Makefile")
# Removed from the makefile:
# Ooops - here I am symlinking tmp.tex -> edrxmain41a.tex... What
# happens if I copy something to tmp.tex later? Does it cease to be a
# symlink, or does it overwrite edrxmain41a.tex?
#
# Possible solution: do not symlink - edrxmain41a.tex has a header
# that explains from where it comes.
#demo1-old: dednat41 texfiles
# mkdir -p $(DEMODIR)
# ln -sf $(DN4EXDIR)/edrxmain41a.tex $(DEMODIR)/tmp.tex
# ln -sf $(DN4EXDIR)/edrx08.sty $(DEMODIR)/edrx08.sty
# ln -sf $(DN4EXDIR)/eedemo1.tex $(DEMODIR)/ee.tex
# cd $(DEMODIR) && $(PWD)/dednat41 tmp.tex
# cd $(DEMODIR) && TEXINPUTS=$(TEXDIR): latex tmp.tex
# cd $(DEMODIR) && ln -sf edrxmain41a.tex tmp.tex
# cd $(DEMODIR) && ln -sf eedemo1.tex ee.tex
#####
#
# dednat4-log.html
# 2008jul12
#
#####
# «dednat4-log» (to ".dednat4-log")
# (find-THgrep "grep -niH -e traffic *")
# (find-blogme3grep "grep -niH -e traffic *")
# (find-blogme3 "anggdefs.lua" "TRAFFIC")
# (find-TH "dednat4")
# (find-TH "dednat4-log")
# (find-es "blogme" "traffic-lights-glyphs")
* (eepitch-shell)
* (eepitch-kill)
* (eepitch-shell)
cd
rm -Rv mkdir /tmp/dn4/
cd ~/dednat4/
make tarball
mkdir /tmp/dn4/
cd /tmp/dn4/
wget http://angg.twu.net/dednat4/dednat4.tgz
tar -xvzf dednat4.tgz
make
make dednat4
make texfiles
make demo2
#####
#
# 2008filterp-texsrc.tar.gz
# 2008jul12
#
#####
# «2008filterp-texsrc» (to ".2008filterp-texsrc")
# http://angg.twu.net/math/
# (find-twusfile "")
# (find-twusfile "math/")
# (find-twusfile "LATEX/")
* (eepitch-shell)
* (eepitch-kill)
* (eepitch-shell)
rm -Rv /tmp/fi/
mkdir /tmp/fi/
cd ~/LATEX/
cp -aiv 2008filterp.{tex,dnt} filters.bib /tmp/fi/
cd /tmp/fi/
~/dednat4/.files.sh eval "{ texedrx ; texother; } | prepends"
cp -aiv $(~/dednat4/.files.sh eval "{ texedrx ; texother; } | prepends") .
rm -v edrxmain*.tex
tar -cvzf /tmp/2008filterp-texsrc.tar.gz *
laf /tmp/2008filterp-texsrc.tar.gz
laf
~/dednat4/dednat4 2008filterp.tex
latex 2008filterp.tex
bibtex 2008filterp
latex 2008filterp.tex
latex 2008filterp.tex
# (ee-cp "/tmp/2008filterp-texsrc.tar.gz" (ee-twusfile "LATEX/2008filterp-texsrc.tar.gz") 'over)
#####
#
# The "lpeg" targets in the Makefile
# 2008jul21
#
#####
# «lpeg» (to ".lpeg")
# (find-dn4 "Makefile" "lpeg")
* (eepitch-shell)
* (eepitch-kill)
* (eepitch-shell)
cd ~/dednat4/ && make tmpdir
cd /tmp/dn4/
tar -xvzf /tmp/dulua.tgz
make S=$S luabuild
tar -cvzf /tmp/dulua.tgz usrc/lua-5.1.3/
make S=$S lpegbuild
./lua51
require "lpeg"
cat > ee.tex <<'%%%'
%D diagram miniadj
%D 2Dx 100 120
%D 2D 100 a^L <= a
%D 2D - -
%D 2D | |
%D 2D v v
%D 2D 120 b => b^R
%D a^L a <= a^L b |-> a b^R |-> b b^R =>
%D enddiagram
$$\diag{miniadj}$$
%:
%: [a,b]^1
%: -------
%: [a,b]^1 b b|->c
%: ------- ------------
%: a c
%: ---------------
%: a,c
%: ---------1
%: a,b|->a,c
%:
%: ^tree1
%:
$$\ded{tree1}$$
%%%
# Local Variables:
# coding: raw-text
# ee-delimiter-hash: "\n#*\n"
# ee-delimiter-percent: "\n%*\n"
# ee-anchor-format: "«%s»"
# End: