#10 deleting from /tmp with /home on a separate fs 7 days ago

Ticket created by ~remexre on ~iptq/garbage

/ and /home are two separate file systems. This causes deletion from /tmp to fail, since a trash can't be made in /.

#9 garbage empty doesn't delete dangling links 9 days ago

Ticket created by ~remexre on ~iptq/garbage

$ ln -s foo bar
$ garbage put bar
$ garbage empty
$ ls -l .local/share/Trash/files
lrwxrwxrwx 3 nathan 24 Jul 15:03 1627156990328.bar -> foo

#5 mdbook+ninja metabug 27 days ago

Comment by ~remexre on ~remexre/stahl

mdbook no longer runs under ninja.

REPORTED RESOLVED FIXED

#5 mdbook+ninja metabug 3 months ago

build-system added by ~remexre on ~remexre/stahl

#5 mdbook+ninja metabug 3 months ago

Ticket created by ~remexre on ~remexre/stahl

mdbook and ninja don't get along too well; noted bugs so far:

• ninja -t clean fails because we can't enumerate the set of files mdbook generates at configure-time
• sites don't get rebuilt when mdbook-repl changes

#8 exit code 3 months ago

Ticket created by ~remexre on ~iptq/garbage

$ garbage put does-not-exist && echo $?
IO error: No such file or directory (os error 2)
0

Should this really be zero?

#6 errors should report relevant file name 7 months ago

Comment by ~remexre on ~iptq/garbage

$ rm tmp out
IO error: No such file or directory (os error 2)

#42 First paragraph of text put above ToC 8 months ago

Comment by ~remexre on ~sircmpwn/man.sr.ht

It's by design: https://git.sr.ht/~sircmpwn/man.sr.ht/tree/0edfb1b70e1c2988fd1545151dfd2f2c36289aef/mansrht/templates/content.html#L40

#4 Literate Stahl 9 months ago

language added by ~remexre on ~remexre/stahl

#4 Literate Stahl 9 months ago

Ticket created by ~remexre on ~remexre/stahl

It'd be quite neat to have a proper literate programming tool for Stahl source code, especially if it would allow the self-hosting implementation's source to be re-used as language documentation. In particular, a major annoyance with reading the current Rust implementation is the degree to which the implementation of a term is spread throughout the code.

To add a new type former requires modifying the definition of the Term and Value types in term.rs and value.rs, adding a few methods to match (some of which could plausibly be generated by a derive macro, others cannot), adding a (trivial) reduction rule in eval.rs, adding a type inference rule in tyck.rs, and adding a parsing rule in elab.rs. Once the reader gets the hang of how these functions all piece together, most of the details of each method are somewhat irrelevant; rather, the useful thing is to be able to see how a term is implemented throughout the language implementation.

WEB-style literate programming is probably the most well-explored idea in this space, but something based on Leslie Lamport's How to Write a Proof is worth exploring too. Especially for systems that can be specified formally, being able to "expand" a high-level prose+code explanation into one that's progressively more complete code seems very useful.