IRC channel logs
2026-06-17.log
back to list of logs
<matrix_bridge><Jeremiah Orians> Added the 2 missing defines in M2libc and fixed the M2-Planet checksums <xentrac>I've been making progress working through the Lean tutorial, which seems like a promising way to get closer to being able to formally verify software <xentrac>despite roconnor's best efforts in the past, I don't really understand the Curry-Howard isomorphism <xentrac>but this is the first time I've been making any effort in that direction in many years <aggi>stabbles: there's not been a hard dependency on linux syscall abi with live-bootstrap in live-bootstrap <aggi>a tcc linked against mes-libc compiling fiwix kernel was able make_bootable this <aggi>the dependency chain in shpack dropped mes-libc and cannot do it anymore hence, because even a minified musl libc.a does need a runtime linux kernel syscall abi <aggi>hence shpack **re-introduced** the linux dependency early into the bootstrapping chain; a problem which already was solved <aggi>this is less of a concern of "trusting trust", but instead after decades of headache at least one such _complete_ bootstrapping dependency chain was re-established <aggi>so far i am not aware of any system-integration for any other ARCH than x86_32 in live-bootstrap <aggi>hence, if shpack/MES-replacement re-considered mes-libc with aarch64 and amd64 for example, this could be very helpful for live-bootstrap to fully support those some time in the future <aggi>another problem i barely recall, was emitting the mes-replacement SL runtime - which is a pre-compiled one still hence does not seamlessly fit into the live-bootstrap dependency chain either <aggi>that's different to mes-cc and a recently introduced alternative pnut-cc <aggi>nonetheless i consider MES-replacement important for another reason: that's been the dependency tracing which frans hacked with it while ago <stabbles>I see, maybe you can open an issue on github.com/FransFaase/MES-replacement <aggi>stabbles: i'm not using github other than git-clone whenever possible <stabbles>from git-clone you can find his email address :) <stabbles>I added another "launcher" to shpack, which builds on the host without chroot, and relies on landlock for isolation from the host file system. The sandbox is a small executable that's just a wrapper around the landlock syscall and is itself bootstrapped, which should be safe, because the executables that are bootstrapped prior to it do not use any <stabbles>system paths. Chroot is of course better cause it's fully hermetic, but unprivileged user namespaces aren't universal, and it's an interesting convenience to be able to run `./store/gcc-16.1.0-hash/bin/g++` directly from the host <stabbles>could also be interesting for software development <roconnor>xentrac: Rocq is better than Lean IMHO, but knowledge of one will likely transfer to the other. <roconnor>What does a hard dependency on linux syscall abi entail? <aggi>roconnor: what does it entail if this dependency is re-introduced _early_ into the dependency chain <roconnor>No. I don't understand what the terminology means exactly. <aggi>and this question was answered already - it introduces a "circular dependency" which blocks entire bootstrapping with it at that stage then <roconnor>What makes some syscall a hard depedency. I thought syscalls were an abstract interface. <roconnor>Like from the beginning of the stage0-posix there are sycalls to open or whatnot. <aggi>sigh, if you think musl-libc can transition back onto builder-hex0 (simplified speaking) then please let us know <roconnor>I don't know anything about the difference between mes-libc and musl-libc. <aggi>roconnor: anyone ever tried to operate musl-libc atop stage0-posix syscall abi? <aggi>M2-libc can, and to mes-libc can; but musl? <nimaje>well, the syscall interface is an ABI, the same syscall number doesn't have to mean the same thing for diffrent kernels and I'm pretty sure UEFI and BIOS don't work with syscalls as there is no kernel <aggi>with regards to musl-libc i've merely patched it to interact with linux-2.4 remaining more conservative <aggi>maybe this too could be be helpful with fiwix one day <aggi>but tbh. i've not been in the mood in recent weeks to re-write all this for configurator/steps <aggi>the ebuild here isn't yet fully synchronized with pass3|4.sh <aggi>without those patches even with a linux2/fiwix syscall interface you would have to expect -ENOSYS thrown all over the place by musl-libc <aggi>even more so when musl was moved onto stage0-posix directly (which i doubt it could be) <aggi>the benefit of fully supporting musl-libc with linux-tcc (2.4) was another though: a complete system integration was feasible with tcc then, no need to bootstrap gcc/binutils early <aggi>and this is what chops most compilation-time finally, removal of gcc/binutils from the early dependency graph <matrix_bridge><Jeremiah Orians> The AI scrappers finally have been rate limited to a point where the boostrapping files service is usable again <roconnor>I don't know what the stage0-posix syscall abi consists of. <xentrac>roconnor: I'm surprised actually at how similar the experience is to Rocq in the Natural Number Game <xentrac>(which uses a sort of simplified Lean interface) <xentrac>in particular there's this thing that I always thought made Rocq proofs hard to understand (without an IDE) in the same way Forth is hard to understand, because you see the sequence of transformations of the terms but not the terms themselves <xentrac>like, the proof that 0 + n = n in the Natural Number Game is: <xentrac>induction n with d pio; rw [add_zero]; rfl; rw [add_succ]; rw [pio]; rfl <xentrac>to read this you have to know that `rfl`, if successful, pops a goal off the goal stack, and that `induction` pushes two goals on the goal stack, so `rw [add_succ]` is acting on the second goal produced by `induction`, `rfl` having dispensed with the first one <xentrac>and it's maybe helpful to know that it's the recursive case of the induction proof, the case where `n` is the successor of some number (which I called `d` here) <xentrac>I'm not sure what the more readable "infix" equivalent would look like <xentrac>but to understand the flow of goals here even in the vaguest terms you need to know the stack effect of each tactic <matrix_bridge><Jeremiah Orians> roconnor: The answer is simple. Values and the syscall are put in registers. The appropriate interruption or syscall is invoked. Only a handful are required up until mes.c (fork, exec, brk, open, close, read, write) <xentrac>(the above code, to clarify, is all Lean, but the same situation obtains with respect to Rocq) <xentrac>oriansj: is that true of shpack too, or does it require a wider variety of syscalls? <matrix_bridge><Jeremiah Orians> I have not dug into the details of shpack yet but there is little reason for it to need more than that (maybe fseek) <xentrac>it seems like that's the claim aggi is making, but I'm not entirely sure. I'm also unsure what "a hard dependency on linux syscall abi" means <xentrac>it seems like it's some sort of problem that keeps shpack from running on fiwix? <xentrac>because it's using musl for early stages rather than mes-libc? <aggi>xentrac: yes. (it's relying upon musl _before_ make_bootable fiwix) <matrix_bridge><Jeremiah Orians> Odd, fiwix implements the same syscalls and unless one is violating the spec; should work identically <aggi>then it would be even more interesting shpack implemented ARCH=x86_32 and test-run this with the full builder-hex0 route taken <alganet>fiwix should be able to run shpack /packages <alganet>the /bootstrap folder is more of a within-linux thing anyways, I see it as a shortcut for those who don't want the full kernel bootstrap <alganet>in that arrangement, something bootstraps fiwix with shpack in it, and shpack takes over from that point mainly for the /packages part <aggi>alganet: sigh. that's among the most interesting pieces, make_bootable any kernel, and if musl-libc could be relied upon as runtime _before_ as the shpack chain implies currently <alganet>but it's also laborious and hard, with no aarch64 and riscv64 alternative for fiwix, so live-bootstrap already fills that niche <aggi>yes, currently the changes made by shpack (musl) could only be fully tested for x86_32 builder-hex0, and there's not been any good reason known yet this ARCH was dropped <xentrac>probably some parts of musl-libc will work on fiwix but maybe some parts use syscalls fiwix doesn't implement <alganet>I know there's a path for musl on fiwix because that's what live-bootstrap does (it's musl 1.1 at that point, I think, and patched) <aggi>then again, musl got run-time injected by shpack _before_ make_bootable fiwix <alganet>because kernel is not on their agenda? <alganet>The way I see it, if someone wants shpack to do kernels, that person integrates and contributes to shpack a change in order, fixes, etc <aggi>the way i see it, live-bootstrap does it just fine already <xentrac>shpack is not an attack on live-bootstrap <alganet>the mes-replacement running on builder-hex0 is an interesting, still unexplored (I think) angle that intersects on this <alganet>I don't know if it was tested on that regime, without a full kernel <alganet>which is something I eventually want to test <aggi>there's the live-bootstrap fork for pnut-cc too, which to my knowledge will run with the full builder-hex0 route taken, and it's too faster than the default mes-cc <xentrac>it *is* important to not rely on the correctness of the Linux kernel, but work that does rely on it can still be useful and important <alganet>also, let's note that "faster" in the full kernel build is way harder. mes does take a huge chunk of the runtime, but so does builder-hex0 (it's slow and needs to run emulated) <aggi>which is no argument anyway, because live-bootstrap (and it's pnut-cc variant) too support the shorter /chroot route <matrix_bridge><Andrius Štikonas> Mes does take a while but moat of the time in live-bootatrap is spent dealing with various pregenerated files <matrix_bridge><Andrius Štikonas> I haven't looked at shpack yet but I guess it doesn't solve those? <alganet>that's another hard thing that is arguibly a choice btw (I too prefer regenerating, although I would consider also rewriting things like autotools as human makefiles) <alganet>but I totally understand the "build it the way it was intended, re-generating everything", which is the sanest way of doing it <matrix_bridge><Andrius Štikonas> Well, rewriting autotools with human makefiles in early projects in live-bootstrap does have one huge benefit <matrix_bridge><Andrius Štikonas> Configure script of e.g. old gzip wouldn't work on riscv <matrix_bridge><Andrius Štikonas> And some people might want something fast <matrix_bridge><Andrius Štikonas> Some other might want everything running using high level language such as scheme