<fossy>ew, just as I go to do the test of the PR addressing all review comments, a new reproducibility bug rears its head <fossy>this time it is the MONTH of the build being coded into the man page <littlebobeep>fossy: What code are you talking about that is not reproducable? <fossy>littlebobeep: it seems that help2man, at least by default, writes into the manpage the month and year that the manpage was generated <littlebobeep>fossy: Ohhh blasted timestamps... I won't be happy until we have no way to tell what year it is in all software <vagrantc>fossy: i thought a fix for that went to help2man upstream... but maybe only patched in debian? or are you using an old version of help2man? <vagrantc>at least, a fix to respect SOURCE_DATE_EPOCH <fossy>vagrantc: it is a old version i believe <vagrantc>for a bootstrap, disabling manpages doesn't seem unreasonable... <oriansj>vagrantc: depends on where in the bootstrap chain honestly. Once one has a Guix or Nix seed, proper man pages and the rest would be expected. Below that, not needed at all. <stikonas>well we disable manpages before help2man was built <oriansj>and could honestly skip help2man entirely and a few more things if one was willing to put in the effort to do so. <fossy>its a 1 line diff to fix help2man, i don <fossy>'t think it's too much of a problem <oriansj>it also depends on how one in to interpret the stated goal of "supported fully functioning operating system" <oriansj>does one need man pages? a web browser? irc client? emacs? <oriansj>muurkha: interesting, no need for gcc just a minimal assembler built by TCC and *BOOM* done <oriansj>muurkha: well there are kernels written in assembly <muurkha>the nand2tetris kids put together a C-level language called "Jack" which is designed to be easy to parse by recursive descent (even easier than Pascal) <muurkha>yup, and plenty of assemblers written in it too <oriansj>muurkha: well M2-Planet's C parser is just 366 lines of C and bootstrapping that in assembly is a straightforward task these days <oriansj>so a kernel written in the C subset that TCC supports also would count <muurkha>I think a hacked version of TCC could do a hacked version of Linux 15 years ago <muurkha>not sure if anyone has gotten tccboot to work with recent versions of Linux <oriansj>but ultimately it is up to fossy and stikonas to decide where the end goal is (unless someone else is willing to carry the work) <muurkha>hope I didn't sound like I thought otherwise <muurkha>I was just saying, tetris is the pinnacle of all software <muurkha>this leads to the uncomfortable conclusion that a Gameboy has a "supported fully functioning operating system" though <oriansj>muurkha: I'm far more partial to warzone2100 <oriansj>I never switch to a distro that doesn't support it <oriansj>muurkha: would indicate one can have tetris without even having an Operating system <muurkha>it claims to be an "OS" but that's a bit of a stretch really <muurkha>it turns out it's not originally or primarily by Óscar Toledo G., he just removed the 386 dependencies <oriansj>back to the original point, perhaps now is the time to maybe make a list of what the final goal pieces would be <muurkha>if you can build gcc or clang you can probably build an irc client or emacs <muurkha>firefox may be a bit tricky due to the rust in servo, not sure how far along bootstrapping rust is <muurkha>I think Chromium is pure C++? probably requires a very recent gcc or clang? <muurkha>at some point the Debian reproducible builds project provides a roadmap <oriansj>well last I checked rust is fully boostrapped (it just is a little memory hungry) <muurkha>that probably covers firefox then? hopefully it doesn't require JS to bootstrap? ;) <oriansj>jquery and the bunch however are pretty fucked right now as far as I am aware, in regards to bootstrappability right now <oriansj>So that could use about 10 years worth of attention <muurkha>that's interesting, what's the problem? can't you run them without minifying them first? <oriansj>muurkha: I must admit I don't know the details but I do know everyone who gets started doing Javascript bootstrapping, quickly gives up. Even those in the Guix/Nix/Debian/Ubuntu/Red Hat/Arch Communitites <nimaje>oriansj: small nit-pick it is (mostly) up to the program to support an os and not the os to support an program, there is some stuff an os can do to make it easier like implementing posix (ok and there is stuff like wine, freebsds linuxemu and wsl) <nimaje>in freebsd ports firefox has a build dependency on nodejs, but no idea what it is used for (where the heck does one find a list of dependencies for building firefox? their docs only say curl and python3, which is obviously incomplete and curl is probably just used to download some of the dependencies) <littlebobeep>nimaje: in gnuzilla.scm in guix there are over 50 build dependcies listed for icecate... including llvm and clang which is strange because it says gnu-build-system <littlebobeep>But further down it specifies clang and clang++ and llvm-ar and llvm-nm env variables for build I don't know why it uses those <oriansj>nimaje: I can see that traditional perspective as entirely valid and generally a good idea <oriansj>however the adoption of KolibriOS, L4Sec and the systemd ecosystem debate seem to indicate the value of compatibility is huge; just like the value of portability for programs is huge as well <oriansj>So it would be reasonable when doing kernel development to be willing provide functionality that you need to run the programs that matter to you. (aka the *BSDs linux compatibility layer, WINE, etc) Either in user or kernel space <oriansj>so for the perspective of a bootstrap kernel (which I will ultimately write in assembly) supporting the bare subset of syscalls needed to get TCC up and running is probably the ideal. As after that a more powerful and complex kernel built by TCC could be used. <oriansj>littlebobeep: the reason for llvm and clang is because they are needed for Rust which is needed to build firefox <muurkha>it wouldn't be terribly surprising if Firefox incorporated LLVM to implement JS, though I haven't heard that it does that <oriansj>muurkha: I have doubts on the ability for anyone to fully understand everything in a 100MB binary <muurkha>me too. you might be able to write ACL2 proofs about it <oriansj>with the number of leaky abstractions required to produce a binary of that size; I have doubts <muurkha>well, the seL4 proofs only rely on the formalization of the part of the CPU instruction set they're using <muurkha>but didn't cover spectre/meltdown as I understand it? <oriansj>muurkha: indeed and were vulnerable to it <oriansj>consider even the trivial case of a C# program using .NET-core; hello-world.cs is a 140MB binary. <muurkha>most of which can be statically proven not to run, presumably <oriansj>muurkha: well no and attacks exist against hello-world.cs <bauen1>the good thing about proofs is that they're very easy (or rather cheap) to verify, so as long as you have hardware that actually does what it says (and what your proof assumes) you will be good <muurkha>another good thing about them is that you don't have to choose which hardware or which software you'll trust <muurkha>you can check the same proof witness with every implementation of Metamath Zero (except the ones that are broken) <muurkha>by contrast, you cannot generate the same binary with every compiler except the ones that are broken <muurkha>and although you may be able to generate the same binary with the same compiler running on different hardware, or the same compiler compiled with different compilers, the binaries can mismatch for innocent reasons if your compiler is written in a language that isn't fully deterministic <muurkha>it's a different approach than the one we've been pursuing though <oriansj>muurkha: very true; formal correctness would be nice to see for future applications but it is an additional layer of work which really doesn't fit in low level bootstrapping. <oriansj>(not that I would reject if someone did formal proofs of correctness for stage0-posix steps) <muurkha>well, it's an alternative approach: write your kernel and compiler and proof assistant in whatever language you like, write your proof witness checker in bare-metal machine code, and then write proofs of the machine code of your kernel and compiler. pretty much what seL4 did <oriansj>muurkha: 510bytes is pretty tight to put a kernel, compiler and proof assistant <muurkha>(at an earlier stage of the project they only wrote proofs of their source code, and I'm not sure if they've done the bare-metal proof witness checker yet) <muurkha>the kernel, compiler, and proof assistant can be however big you want, written in any language you want <muurkha>and you don't have to run the proof witness checker on an IBM PC either <oriansj>muurkha: the root bootstrap seed for x86 hardware can't be larger than 510 bytes <muurkha>right, but you can run the proof witness checker on non-x86 hardware. you can burn a PROM with it if you want <oriansj>hence the suggestion it being done in a later stage for simplicity <oriansj>aka it is much easier to do with TCC or even just the M2-Planet C subset than having to do it in hex0 ***genr8eofl__ is now known as genr8eofl
<muurkha>yeah, but what I'm saying is that it's not a different stage of the same process, it's an alternative approach to solving the same problem