Here I leave messages to the world, myself and our future robot overlords.EOF
Isabelle/ML is a strange programming environment for writing code that can also interact with Isabelle theories. The basic example of this is the idea of antiquotations (a kind of preprocessor) that allows referring to terms defined in theories. In the following snippet the command ML_val inteprets the text as a Isabelle/ML program. The only interesting detail here is that the @{term "HOL.conj"}…
Nginx can be a bit of a bother to configure, especially since I want to buy in the configuration that my distribution provides. On my Debian box, this is what the configuration layout looked like when I started. In the rest of this post, I will omit parts of the configuration that are not relevant. # tree -d /etc/nginx/ /etc/nginx/ ├── conf.d ├── modules-available ├── modules-enabled ├──…
You should spend some time in immutable Linux land , you might like it. When starting my PhD I got handed a laptop and told to set it up. At the time I chose OpenSUSE Aeon as I was familiar with Tumbleweed. This was a fantastic choice and for the kind of work I do and I don’t regret it. Removing the burden of system administration is a value I can get behind and I think it really paid off. Each…
Isabelle/HOL is an interative theorem prover. To be extremely precise Isabelle is a distribution of a the theorem prover and HOL is an object logic embedded in the ambient logic. If this is confusing don’t sweat about it, it’s only to make the next distinction a little clearer. I have recently started a project using Isabelle/ML, the part of the Isabelle distribution where you write Standard ML…
Bob complains that starred commands in LaTeX can have a better user-experience . This actually sent me back in time to younger edoput trying to understand why some scheme functions are suffixed with ‘*’, e.g. append* . Two instances don’t make a pattern but I’m wondering if there’s a third programming language where * is also used in identifiers with the same intent, “like this other thing, but a…
There was one huge pain point during the development of gotobed : I would put in bugs without knowing and things would go bad. A plugin is effectively a smaller application that is embedded into Koreader but Koreader did very little to point out what went wrong in case something goes wrong. This behavior is actually implemented by the following piece of code. At plugin load time the function…
I really like typesetting with unicode math symbols. I use them in my notes, sometimes even in LaTeX as we get the unicode-math package. To input unicode symbols in Emacs I use the unicode-math package and before that my own-grown input method. The input method is bound to a buffer so when you switch (intentionally or not) to another buffer typing \alpha will not result in a pretty α being…
Recently I read this beginners guide to extend Emacs . The guide is perfect for starting out with elisp and it shows a lot of care in teaching how to interact with Emacs. To me, the most important bit though is this one, from the section aptly named Emacs Wants You to Extend It . I haven’t written plugins for other editors extensively, but I can tell you this: emacs doesn’t just make deep…
Loading values from the environment into variables is a way to configure processes at startup. Alternatives are to define a command-line interface or parsing configuration files. Each of these methods has its advantage but loading values from the environment has a shortcoming. As an operator you have to refer to the documentation of the tool as there is no interface to query what the process…
Running MicroOS as my daily on the work laptop is quite the experience. Nothing ever breaks but at the same time there is very little that can. This is because the apps I need are not packaged. Sad. Over time I have packaged what I need but one of them took some time. VisualVM is a GUI to troubleshoot your Java processes, as it requires the Java SDK and Java SRE at runtime I was not sure how to…