<fossy>dosen't really matter the order <stikonas>hmm, perl has some Configure file to do build <OriansJ>*Is confused how M1/M0/hex2/hex1/hex0 is hard to verify* <fossy>OriansJ: hard to understand without appropriate background knowledge of the architecture <OriansJ>stikonas: cc_* is always in M0-macro assembly (as indicated by the DEFINEs and lack of crossplatform support) <fossy>but that is just the nature of such low level <OriansJ>fossy: and the NASM versions probably don't help much either <OriansJ>but I do have C code versions of all of the steps as well <fossy>OriansJ: not if you want to verify the bootstrap from teh ground up <OriansJ>markjenkinsznc has some python version if I remember correctly. <OriansJ>to civodul's question about source; nothing lower than M2-Planet in the bootstrapping stack is in a preferred form for modifications. As writing Assembly always sucks; it just sucks less than trying to write those pieces in FORTH. <OriansJ>hence why hex0, hex1, hex2, M0 and cc_* are barely touched after creation. <stikonas>it uses <sys/signal.h> but we only install it to signal.h, should I patch / sed it or do we want to install it there too? <ericonr>stikonas: if you install something into sys/signal.h, it should be a header that just does "#include <signal.h>" <stikonas>ericonr: yeah, but m4 includes #include <sys/signal.h> <fossy>i dont really care, whatever you like <stikonas>ok, I think Perl's Configure is handwritten <stikonas>but it's 25K lines of shell scripting... <xentrac>what, did the "Congratulations, you're not running Eunice." tip you off? <stikonas>there is this thing: +# Generated on Tue Sep 12 17:23:02 EET DST 2000 [metaconfig 3.0 PL70] <stikonas>ok, I think I'll have to work with much older perl <stikonas>which have very few c files and can probably be built manually <xentrac>stikonas: the Perl building process starts by building a thing called "miniperl" <xentrac>at least last time I ran it, which I'm pretty sure was more recent than Perl 5 <xentrac>not sure if it's powerful enough to build Configure with <xentrac>no, but if you run Configure I think you'll probably observe it <stikonas>hmm, it looks like miniperl is perl without ability to load dynamic shared modules <stikonas>maybe that's good enough to drive autotools... <xentrac>how much of configure do you need to run before you can build minnie pearl? <stikonas>well, in principle we can run configure... <stikonas>well, maybe one can write makefile to build miniperl... <stikonas>altough, perl's configure is still more "source'y <stikonas>but I guess not good enough for "full" bootstrapping <stikonas>well, I guess the way to go is to write custom makefile for miniperl... <stikonas>miniperl is built fairly early when you run make <fossy>stikonas: do you have any idea why i might be getting an absolute ton of undefined symbols wehn linking bash <fossy>my rule is $(CC) -o bash $(LDFLAGS) $(LIBRARIES) $(OBJS) -lsh -lbuiltins -lglob -ltilde <fossy>libsh.a libbuiltins.a libglob.a libtilde.a <fossy>the only relation i can find between all of them is that they all have externs <fossy>some arent even in libraries <stikonas>well, maybe push something to work branch <stikonas>fossy: ok, I have working m4, do you want a new PR? <stikonas>otherwise it's hard to do PR on top of PR... <stikonas>fossy: by the way you can probably delete "patch" branch now <stikonas>fossy: I'm getting ./mksyntax -o syntax.c <stikonas>probably something bad in Makefile withthat mksyntax object <fossy>it was MKBUILTINS instead of MKSYNTAX_OBJS <stikonas>ok, I'm getting getopt optarg and optind undefind symbols here <stikonas>I get the same error when running normal configure <fossy>stikonas: i know what the mksyntax problem was <fossy>i forgot to link against getopt (did it in testing but not in the makefile) <fossy>what, that didn't happen even when i ran the makefile in the thing <fossy>and this is a direct copy of it now... <fossy>i'm thinking the copy-paste was not completely successfull <stikonas>not sure if I'll have time before bed though <fossy>that's fine, i'll look at it later today anyway <stikonas>I'll check tomorrow if you are still not done <deesix>OriansJ, the 'TMP' branch of my M2-Planet repo has test0021 adapted to use M2libc. Feel free to cherry-pick bcd0f498591521ddbcb43456142c8beab964a9f0 <deesix>Now that all (but test1000) are done, I'll use AArch64 as the base of script unification, during the following days. <xentrac>metamath zero is a proof checker; you feed it proofs you have constructed by some other means (probably an interactive proof assistant) and it verifies that they prove what you say they do. the proposal there is to formalize enough of the x86 instruction set that MM0 can verify itself <fossy>gforce_d11977: yes, but none of the required code is there <fossy>gforce_d11977: for example, we only copy x86/ in, and idk if wip-m2 works on arm fully, or if tcc is up to the required standard <fossy>signfiicant progress on bash <fossy>stikonas[m]: it was not defines <fossy>it was simply the required symbols were not there, for whatever reason <fossy>(including: a missing object on the command line, mkbuiltins clobbering files, etc <gforce_d11977>fossy: ok, but the progress for aarch64 is more complete, is'nt it? <fossy>gforce_d11977: idk.. more so than arm in M2-Planet/mescc-tools, but i think less so in tinycc, janneke can correct me on that <fossy>but much less complete than x86 for sure <janneke>right, mes, mes libc and bootstrappable-tinycc have support for arm, although gcc-4 isn't bootstrapped yet <bauen1>xentrac: that's very intersting, reminds me of how some math problem was solved, a huge complicated automated proof assistant (?) that nobody really understood, and a very small well understood and verified proof checker (i think coq) <bauen1>would a bootstrap kernel need to support SSE or floating point operations, or can you compile linux (and its dependencies) without it ? <bauen1>or rather does printf need to support the 'e', 'f' values <bauen1>just needing to decided if i want to implement sse userspace support or just strip out anything "float" related from musl libc <bauen1>alright, wasn't too hard to strip it out, so i'll just go that way for now <fossy>stikonas: very nearly almost <fossy>after i merge bash i'll move m4 to the bash script <fossy>one thought, maybe we should include a mk/ directory like we do for patches <stikonas>hmm, maybe we need to think how to put everything, not just make files *fossy is confused what patch you mean <stikonas>fossy: so I'm fine with mk directory, although, it might be nice to put all build scripts there... <stikonas>hmm, on the other hand, some kaem files are more complicated (tcc kaem files work with multiple folders) <siraben>xentrac: Haskell is definitely powerful enough to implement a metamath checker <siraben>heh wouldn't that be fun later, bootstrap mathematics AND compilers <bauen1>siraben: i think that would be a very good idea, from my limited understanding of formal methods they also rely on all the underlying compilers / kernels / libcs to be "bug-free" <siraben>yes, they also need trusted cores. Coq's core is only a few hundreds lines IIRC <siraben>You can't prove the consistency and completeness of a sufficiently expressive theorem prover within itself, Gödel strikes again! <stikonas>fossy: we also need bison before autotools <stikonas>I'll see if I can workaround it with different versions... <xentrac>siraben: you can implement a metamath checker in any programming language pretty easily ***ChanServ sets mode: +o rekado_
***rekado_ is now known as rekado
<xentrac>there are a lot of different metamath verifiers, the idea being that we'd like to not depend on a single possibly buggy and exploitable program to check a metamath proof <xentrac>to tackle the problem bauen1 mentioned, the current proofs of seL4 (in Coq) verify not just the source code (of the kernel!) but the executable code, although they fail to verify if you use sufficiently high optimization levels <xentrac>the idea there is that by presenting a proof of correctness of a particular Metamath verifier (in x86 machine code, again, not source code) you can use any other Metamath verifier on *one* proof to verify that the x86 executable is correct for *all* proofs <xentrac>I don't know if there's a proof of consistency of the Metamath Zero core language that these verifiers verify, but certainly it is not intended to be complete <xentrac>so there are presumably theorems that are true but which Metamath Zero cannot prove; we hope that those theorems don't happen include too many theorems of interest <OriansJ>gforce_d11977: although I have prototyped the steps for armv7l; I have not actually converted them into hex0, hex1, hex2 and M0. <OriansJ>Which is not a small task and is rather tedious <OriansJ>which at this moment isn't a top priority to get it done. <OriansJ>bauen1: well in absolute terms. Compilers don't require floating point support from an engineering standpoint but some compilers do use it for fuzzy approximation to do some things faster. <xentrac>or for compile-time constant folding <xentrac>when they're compiling code that uses floating-point support <OriansJ>xentrac: wouldn't that fall under doing some things faster? <siraben>xentrac: thanks for that information, I'll look into it <bauen1>OriansJ: true, in absolute terms you also don't need a compiler :) <xentrac>OriansJ: yes, but not by way of fuzzy approximation <gforce_d11977>OriansJ: sorry no pressure, armv7l comes later 8-) for now, there enough polishing to do for x86_64, x86, the rest comes later, and maybe *someday* i will do the lowlevel stuff for MOS6502 and m68k 8-))) <fossy>wrt bison, I just realised bash and patch are shipping precompiled bison parsers <fossy>we should follow gios bootstrapping path for flex and bison <stikonas>I noticed that when I tried to build gawk <stikonas>fossy: bison is a bit tricky but probably not impossible <stikonas>fossy: what file is precompiled in patch? <stikonas>I don't see anything in patch at first glance <fossy>stikonas: I think it is called y.tab.c <stikonas>I ran in our sources dir for file in *; do lsar $file | grep '\.y'; done <fossy>well we cab disable that, surely <stikonas>so good that we didn't move sed after tar <stikonas>anyway, we need to bootstrap bison 3.4.1 <fossy>bash is nearly done, I didnt get anything more done since my last status update <stikonas>ok, I think it's not the end of the world... <stikonas>some quick attempt showed some problems with getprogname <stikonas>and I thought people in early days of GNU cared about bootstrapping more than now... <fossy>read the last 4 dot points in that section <fossy>we need bash for autotools I think <fossy>but dash would work for a bit <fossy>so the primary issue is bash... <fossy>hm, maybe dash is sufficient to run a configure script <fossy>it seems to be on my host system <stikonas>but that doesn't solve autotools bootstrap issue <stikonas>it's just that we can get some shell earlier <fossy>we need a shell for a number of features <fossy>and we need bison for autotools <fossy>well, i guess i'll finish bash and leave the PR open <fossy>then i'll do dash instead, then we can do the flex/yacc/bison dance <stikonas>since I already have submodule imported in a local branch <stikonas>fossy: or actually any other shell would work too... but I guess dash might be simplest... <fossy>stikonas: dash is probably simplest, yea <stikonas>fossy: I think our libc is insufficient to compile heirloom tools lex/yacc <stikonas>ldefs.c:46: error: include file 'wctype.h' not found <fossy>stikonas: odd, might be able to disable it... <OriansJ>gforce_d11977: well the 68K could definitely run the steps for bootstrapping GCC but the 6502 would have to do a sweet-16 to run cc_* without some serious modifications as the 6502 has a rather small hardware stack (256Bytes) <fossy>bash links now but segfaults on startup <stikonas>fossy: well, we need bison for bash anyway... <stikonas>we can later compile bash using configure