my forest
weeknotes, add code highlighting, start isabelle notes.
+133
-1
assets/wetlands1.jpeg
assets/wetlands1.jpeg
This is a binary file and will not be displayed.
assets/wetlands2.jpeg
assets/wetlands2.jpeg
This is a binary file and will not be displayed.
+4
trees/isa-0001.tree
+4
trees/isa-0001.tree
+1
trees/loc-001B.tree
+1
trees/loc-001B.tree
+1
-1
trees/loc-0023.tree
+1
-1
trees/loc-0023.tree
+26
trees/loc-0027.tree
+26
trees/loc-0027.tree
···
1
+
\import{table-macros}
2
+
\def\percent{\startverb%\stopverb
3
+
}
4
+
\parent{loc-000P}
5
+
\title{22nd Sunday after Pentecost 2025}
6
+
\tag{cmc}
7
+
\date{2025-11-09}
8
+
\author{liamoc}
9
+
\quote{
10
+
Intret orátio mea in conspéctu tuo: inclína aurem tuam ad precem meam Dómine.
11
+
}
12
+
\p{This Sunday I directed our choir at [All Saints Ainslie](https://allsaintsainslie.org.au) for Purcell's [Thou Knowest, Lord](https://www.youtube.com/watch?v=ACqaMARAmZk):}
13
+
\quote{
14
+
\poem{
15
+
\line{Thou knowest, Lord, the secrets of our hearts:}
16
+
\line{Shut not, shut not thy merciful ears unto our prayer,}
17
+
\line{But spare us, Lord. Spare us, Lord most holy.}
18
+
\line{O God! O God most mighty! O holy and merciful Saviour,}
19
+
\line{Thou most worthy judge eternal,}
20
+
\line{Suffer us not, suffer us not at our last hour,}
21
+
\line{For any pains of death to fall from thee.}
22
+
\line{Amen.}
23
+
}
24
+
}
25
+
\p{We also had a brief meeting yesterday morning to discuss our future plans for the choir. We have some exciting music ahead, and some of us agreed to sing at a special service at Goodwin Retirement Living for the residents there during Advent. Next year at the church, we plan to have semi-regular concerts, and I will also be forming a small group to sing regular Evensong services.
26
+
}
+41
trees/loc-0028.tree
+41
trees/loc-0028.tree
···
1
+
\date{2025-11-09}
2
+
\title{ITP course at the ANU Logic Summer School}
3
+
\author{liamoc}
4
+
\p{As [I previously mentioned](loc-001W), I am teaching at the ANU Logic Summer School this year, on an introduction to interactive theorem proving using the proof assistant [Isabelle](https://isabelle.in.tum.de). Here's the course blurb as found on [the website](https://comp.anu.edu.au/lss/lectures/2025/):}
5
+
\subtree{
6
+
\title{Abstract}
7
+
\p{This course will introduce the use of interactive proof assistants both for mathematics and for work in software verification. We will introduce the basics of interactive theorem proving using the proof assistant Isabelle/HOL. Starting from elementary logical formulae, we will prove many theorems “live” in lectures, and apply what we have learned to proof exercises and challenges. Proof assistants can be both very fun and very addictive in equal measure. It is my hope to share that fun with you.}
8
+
}
9
+
\subtree{
10
+
\title{Topic list (tentative)}
11
+
\ol{
12
+
\li{Propositional and first-order logic, natural deduction proofs. Types, definitions, unfolding.}
13
+
\li{Simplifier, rewriting, function definitions, other definitions.}
14
+
\li{Structural induction, inductive definitions, induction tactics.}
15
+
\li{Structured proofs in Isar, calculational proofs.}
16
+
\li{More automatic methods, sledgehammer.}
17
+
}
18
+
\p{Remaining topics to be covered if there is time:}
19
+
\ul{
20
+
\li{General recursion and termination measures}
21
+
\li{Type classes and locales}
22
+
\li{Program verification with SIMPL or AutoCorres}
23
+
\li{Designing tactics with Eisbach}
24
+
}
25
+
}
26
+
\subtree{
27
+
\title{Prerequisites}
28
+
\p{Some familiarity with simple first order and propositional logic is assumed. Some functional programming experience (in particular, some familiarity with lambda calculus or a language like Haskell) is also recommended.}
29
+
}
30
+
31
+
\subtree{
32
+
\title{Recommended Further Reading}
33
+
\p{[Concrete Semantics](http://concrete-semantics.org/), [[nipkow]] and [[gklein]]}
34
+
}
35
+
\subtree{
36
+
\title{Lecturer}
37
+
\p{[[liamoc]] is a Senior Lecturer at the [[anu]] and an Honorary Fellow at the [[uoe]], where he worked until 2024. He obtained his PhD from UNSW in 2019, the [dissertation](oconnor-thesis-2019) for which received the John Makepeace Bennett award. He has broad interests in theoretical computer science, especially in semantics, models and specifications, as well as in the application of these theoretical techniques to practical problems in programming languages, systems and software engineering.}
38
+
}
39
+
\p{I will also make the [course notes](isa-0001) available on this forest, as they are completed.}
40
+
41
+
+26
trees/loc-0029.tree
+26
trees/loc-0029.tree
···
1
+
\import{shiki-macros}
2
+
\date{2025-11-09}
3
+
\title{Syntax Highlighting in Forester for Isabelle (and More)}
4
+
\author{liamoc}
5
+
\p{Similar to my [theme plugin for Gregorian Chants](loc-0015), I've implemented a simple plugin for syntax highlighted blocks using the [Shiki](https://shiki.style) library. Unlike the chant plugin, it doesn't self-host all the required JS but instead loads from a CDN. If this becomes problematic later I will investigate self-hosting it, but it seems that self-hosting Shiki is somewhat complicated. }
6
+
\p{I didn't use any other syntax-highlighting gizmos for Forester because I plan to write [lecture notes](isa-0001) for my upcoming [course at the LSS](loc-0028) and this would require me to support Isabelle code. The advantage of Shiki is that it supports textMate grammars, and [[gklein]] made [one for Isabelle](https://github.com/lsf37/Isabelle.tmbundle).}
7
+
\p{Like the chant plugin, it consists of a single drop-in module of JavaScript, some changes to the stylesheet and a macro definition tree. As can be seen below, the results are quite nice:}
8
+
\put\shiki/language{Isabelle Theory}
9
+
\shiki{theory Main imports Pure
10
+
begin
11
+
typedecl bool
12
+
judgment Trueprop :: ‹bool ⇒ prop› ("(_)" 5)
13
+
14
+
axiomatization
15
+
False :: ‹bool› and True :: ‹bool› and
16
+
conj :: ‹bool ⇒ bool ⇒ bool› (infixr "∧" 35) and
17
+
disj :: ‹bool ⇒ bool ⇒ bool› (infixr "∨" 30) and
18
+
implies :: ‹bool ⇒ bool ⇒ bool› (infixr "⟶" 25) and
19
+
not :: ‹bool ⇒ bool› ("¬ _" [40] 40)
20
+
where
21
+
(* Conjunction *)
22
+
conjI : "⟦ A ; B ⟧ ⟹ (A ∧ B)" and
23
+
conjunct1 : "A ∧ B ⟹ A" and
24
+
conjunct2 : "A ∧ B ⟹ B"
25
+
end}
26
+
\p{(If it doesn't display correctly, you may need to clear your browser cache.)}
+6
trees/people/nipkow.tree
+6
trees/people/nipkow.tree
+4
trees/places/tum.tree
+4
trees/places/tum.tree
+11
trees/shiki-macros.tree
+11
trees/shiki-macros.tree
···
1
+
\xmlns:html{http://www.w3.org/1999/xhtml}
2
+
3
+
\def\shiki/loadLanguages{c,javascript}
4
+
\def\shiki/rootPath{/forest}
5
+
6
+
\alloc\shiki/language
7
+
\def\shiki[body]{
8
+
\scope{
9
+
\<html:shiki-block>[language]{\get\shiki/language}[load-languages]{\shiki/loadLanguages}[root-path]{\shiki/rootPath}{\body}
10
+
}
11
+
}
+13
trees/weeknotes/2025-W45.tree
+13
trees/weeknotes/2025-W45.tree
···
1
+
\import{table-macros}
2
+
\title{Weeknotes 2025-W45}
3
+
\author{liamoc}
4
+
\date{2025-11-09}
5
+
\p{This week was mostly occupied with various administrative catchups after my two weeks of leave. }
6
+
\figure{
7
+
\<html:img>[width]{240px}[src]{\route-asset{assets/wetlands1.jpeg}}{}
8
+
\<html:img>[width]{240px}[src]{\route-asset{assets/wetlands2.jpeg}}{}
9
+
\figcaption{Some nice sunsets near the Lyneham wetlands.}
10
+
}
11
+
\transclude{loc-0028}
12
+
\transclude{loc-0029}
13
+
\transclude{loc-0027}