thaliaarchi

readtape has now been updated for portability.

Unix V1 also used 1/60 seconds

I was talking about the performance, not the feature set. Russ Cox's re1 and the re1.5 fork have several engines for different implementation strategies. re1 was written for primarily pedagogical reasons, so its minimality comes from that.

The engine chosen by MicroPython is vulnerable to catastrophic backtracking and switching to the Pike VM implementation would fix that. Instead of backtracking in the text when the pattern doesn't match, the Pike VM iterates each char in the text only once, visiting the states valid for that position in lock step. Consequently, it allocates a list of “thread”s, proportional in length to the number of states in the pattern (though usually patterns have relatively few states). Many security issues have resulted from regexp denials of service, so this slight memory tradeoff might be worthwhile.

Since recursiveloop.c has been changed by MicroPython, those changes would need to be ported to pike.c. The fixes are small and none of the extra features exploit the backtracking, so this should be easy.

I find it interesting that MicroPython's `re` module[0] is implemented with a backtracking regular expression engine from re1.5[1], instead of one of the linear-time engines from the same library. (Russ Cox covers the various engines in the excellent blog series[2] which re1 is a companion to.) I figure the choice was made due to binary size or memory constraints, though they're all quite small.

[0]: https://github.com/micropython/micropython/tree/master/lib/r...

[1]: https://github.com/pfalcon/re1.5/tree/v0.8.2

[2]: https://swtch.com/~rsc/regexp/regexp2.html

I just built my PiDP-11 and would love to get one of these.

Simple format. Makes me want to write a parser for it using a shared buffered reader library I’m working on in Rust.

I'm continuing my tradition of doing AoC in Whitespace[0]. The first year I did it, it was motivation to build out a standard library so things wouldn't be so tedious. Now, I find myself wishing I had finished better tooling. I debug with wsjq[1], a CLI debugger like gdb written in jq, but it's slow.

[0]: https://github.com/thaliaarchi/ws-challenges

[1]: https://github.com/thaliaarchi/wsjq

The current article[0] says:

> Excel 2.0 was released a month before Windows 2.0, and the installed base of Windows was so low at that point in 1987 that Microsoft had to bundle a runtime version of Windows 1.0 with Excel 2.0.

[0]: https://en.wikipedia.org/wiki/Microsoft_Excel

Or easier, do an interactive rebase and mark the last commit which is in the partial-rebase branch for editing. Then, do `git reset --hard partial-rebase` and continue the rebase.

That feeling seems common in hindsight. Everything seems easier, once all the problems have been solved. Related, I enjoy the author's sense of humor:

> I made a prototype and, lo and behold, it was in fact slow, as predicted. (I’m smart.)

And in another article[0], describing an inefficient collision algorithm:

> Mojang’s decision never crossed my mind. I guess I’m not a real programmer.

[0]: https://purplesyringa.moe/blog/ru/minecraft-compares-arrays-...

That explains why there’s so many Swiss APIs.

I use the following to create a commit using the latest modification date of the staged files. If you put it in your PATH as git-tcommit, you can invoke it as `git tcommit`. If GIT_AUTHOR_DATE or GIT_COMMITTER_DATE is passed, it overrides the modified time, and it honors TZ. It works with GNU or BSD.

    #!/usr/bin/env bash
    set -eEuo pipefail

    # `git commit`, using the latest file modification time as the commit and author
    # dates, when GIT_AUTHOR_DATE or GIT_COMMITTER_DATE, respectively, is not set.

    # Use fractional seconds when available to display the newest file more
    # accurately, even though Git only uses seconds.
    if which gstat >/dev/null; then
      stat=(gstat --format='%.Y %n') # Detected aliased GNU coreutils
    elif stat --version 2>/dev/null | grep -q 'GNU coreutils'; then
      stat=(stat --format='%.Y %n') # Detected GNU coreutils
    else
      stat=(stat -f '%m %N') # Fallback to BSD-style, which only reports seconds
    fi

    # Select the latest modified time of all staged files, excluding deletions.
    modified="$(
      cd "$(git rev-parse --show-toplevel)" &&
      git diff --staged --diff-filter=d --name-only -z |
        xargs -0 "${stat[@]}" |
        sort -rn |
        head -1
    )"

    modified_seconds=
    if [[ -n $modified ]]; then
      modified_seconds="${modified%% *}"
      modified_file="${modified#* }"
      modified_date="$(date -r "${modified_seconds%.*}" +'%Y-%m-%d %H:%M:%S %z')"
      echo "Modify date: $modified_date ($modified_file)"
    fi
    author_seconds="$modified_seconds"
    committer_seconds="$modified_seconds"
    if [[ -n ${GIT_AUTHOR_DATE+.} ]]; then
      echo "Author date: ${GIT_AUTHOR_DATE:-now}"
    fi
    if [[ -n ${GIT_COMMITTER_DATE+.} ]]; then
      echo "Commit date: ${GIT_COMMITTER_DATE:-now}"
    else
      last_commit_seconds="$(git show -s --format=%at HEAD 2>/dev/null || echo 0)"
      if [[ $modified_seconds < $last_commit_seconds ]]; then
        committer_seconds=
        echo "Commit date: now (last commit: $(git show -s --format=%ai HEAD 2>/dev/null))"
      fi
    fi

    GIT_AUTHOR_DATE="${GIT_AUTHOR_DATE-"$author_seconds"}" \
    GIT_COMMITTER_DATE="${GIT_COMMITTER_DATE-"$committer_seconds"}" \
    exec git commit "$@"

This was also a year before Mad Libs was invented in 1953, using the same template-filling style.

> The resulting units may be called binary digits, or more shortly, bits.

It's interesting to read this early use of “bit”, before the term became commonplace. The first publication to use “bit”, also by Shannon, was only a year prior[0].

[0]: https://en.wikipedia.org/wiki/Bit#History

Edited. Thanks

A compiler that injects backdoors in targeted programs and self-propagates the meta-backdoor (to avoid detection in the source) is exactly the trusting trust attack and it can be mitigated by diverse double-compiling (paper linked above). It requires a second compiler and we have mrustc, a Rust compiler in C++ built specifically for circumventing the unverified bootstrap chain of rustc.

The process is: Compile mrustc with a C++ compiler. Compile rustc sources with untrusted rustc binary and compile rustc sourcs with mrustc (these have identical behavior, but different codegen). Compile rustc sources with rustc-by-rustc and compile rustc sources with rustc-by-mrustc (these will have identical behavior and codegen). Those will match. If you compile once more, they will match. Since mrustc is never compiled by rustc, such a backdoor would have to also exist in gcc/clang and propagate with exactly identical behavior in mrustc. The process could be repeated for gcc/clang.

I didn't touch on that, but I did assume trust of the Rust toolchain, verifying starting at THIR. Verifying rustc would be a monumental undertaking, though I think some people are working on it.

Since we don't have a verified rustc (a la CompCert [0]), I wonder if an approach like the translation validation of seL4 [1] would work. They prove that the artifact (ARM machine code) produced by an existing compiler (gcc) for a chosen program (seL4) matches the source semantics (C). Thus you could circumvent trusting rustc, but it only works to verify a specific output of a chosen program. If the chosen program was coq-of-rust, I don't think this would be easier than the approach I detailed above. The seL4 kernel is 9,500 lines of C, while their Isabel/HOL specification is over 200,000 lines, so the technique doesn't seem to scale to a large chosen source like rustc.

Isn't bootstrapping fun?

[0]: Xavier Leroy. 2008. “Formal verification of a realistic compiler”. https://xavierleroy.org/publi/compcert-CACM.pdf

[1]: Thomas Sewell, Magnus Myreen, and Gerwin Klein. PLDI 2013. “Translation Validation for a Verified OS Kernel”. https://sci-hub.st/10.1145/2491956.2462183

That's really impressive.

Automatic translation like this shifts the trust to the tool. coq-of-rust itself is written in Rust, not in Coq. The recursive nature is somewhat boggling, but I think a proof of its correctness is possible in a similar process to David A. Wheeler's “Countering Trusting Trust through Diverse Double-Compiling” (2009) [0] (which circumvents Ken Thompson's Trusting Trusting attack by using a second compiler), but with a mix of a CompCert approach.

To verify it, you'd use coq-of-rust to convert the coq-of-rust translator from Rust to Coq. That translation is not trusted, because it was performed in Rust, but it doesn't matter. Once in Coq, you prove the desired correctness properties—crucially, that it preserves the semantics of the Rust program when it translates a program to Coq.

As in the article, it is likely easier to work with more functional definitions in proofs instead of generated ones, so you'd undertake the same process as they do with the stdlib of proving equivalence between definitions. Since the current line count for the coq-of-rust translator (specifically, lib/ [1]) is 6350 lines of Rust, it even seems feasible to write a full translator in Coq and prove its equivalence to the generated one.

Then, you execute the proven-correct Coq coq-of-rust translator on the Rust source of the coq-of-rust translator. The Coq definitions it outputs should match the output of the Rust coq-of-rust translator that you started with.

As an aside, it's nice to see industry funding for work like this. I'm often cynical of cryptocurrency, but its correctness constraints really push for improvements in areas I like (Rust, Coq, funding for masters students I know, etc.).

[0]: https://dwheeler.com/trusting-trust/wheelerd-trust.pdf

[1]: https://github.com/formal-land/coq-of-rust/tree/main/lib

You might try building Ruffle from source. I’ve found that online versions don’t work for the games I want, due to using an outdated version of Ruffle.

What’s the context for “Do Not Install”?

> Out in the literature we can find a huge number of dataflow analyses, some of which are useful to optimize some kinds of code — but it’s hard to know which ones to actually implement. […] First, implementing the analysis itself, which requires creating an abstract version of each instruction in the compiler’s IR: these are called dataflow transfer functions. For example, to implement the addition operation for integer ranges, we can use [lo1, hi1] + [lo2, hi2] = [lo1 + lo2, hi1 + hi2] as the transfer function.

What papers would you recommend for learning implementing dataflow analysis? For example, foundational or tutorial papers.

> Replace your docs

> Developers don't like writing docs. Now, they don't have to!

Well that’s a terrible premise. AI can’t get at design decisions or anything that’s not explicitly encoded in code, but still connected. The “why” is extremely valuable.

> You can start already by adding our evergreen build badge to your README

I can do that easy! Just use a static image for the badge!

This got me thinking about what the Linux kernel was using before BitKeeper (of course before Git). Did it not have version control? Was it just Torvald's tree, maintained by applying patches from the list, and distributed via archives or rsync? (Oh, and if anyone knows how to get a copy of the BK or pre-BK sources, let me know!)

A strange case I've run across from the SCCS and RCS era is Plan 9. The history of the Plan 9 kernel is stored as ed scripts[0], which produce revisions per file, essentially like ad hoc SCCS deltas. I'm not sure if it was assembled as such after the fact or recorded like that all along. That method seems to have only been used for the kernel and the rest (such as the libraries) was snapshotted daily on a file server starting in 2002.

[0]: https://9p.io/sources/extra/9hist/README (To look around, just pop off README.)

I’ve never heard of a Jpegli bread, but Zöpfli and Brötli sure are yummy :)

Do you still have a record of any of those weird case repos? Perhaps reported as issues somewhere? I’m working on a tool like git filter-repo and Reposurgeon combined and would love stress tests and edge cases like these.

Any plans to tackle the Python version installation side of things and make it as seamless as rustup has? I've previously used `pyenv install` for this, but it would be nice to fold it into one tool.