IRC channel logs
2021-06-07.log
back to list of logs
<Melg8[m]>btw what are currently active bootstrapping projects with baremetal or bios - as starting point - with x86 as target platform? <Melg8[m]>@gio i tired to run master branch of asmc and it gives me error: "Parsing MM0 theory: delimiter ASSERTION FAILED" why that happening? <gio>Melg8[m]: I am not aware of other projects like asmc and, as you see, I have not been able to work on it for quite some time. <gio>That should still be working. <Melg8[m]>@gio yea, why is that? did you learned some flaw in your approach or just have less time to work on it? <gio>Melg8[m]: Mostly I bootstrapped a daughter and started a new job. <Melg8[m]>@gio yea... i checked your facebook and from there, thought that now you have another project going))) btw, i just glanced on asmc - but looks very impressive. What the idea behind mm0? what you try to verify with it and why? <Melg8[m]>one thing that bothers me - i watched your presentation from 2019 - you said that bios -> bootloader -> than asmc - is that correct now? or you created image with mbr - and it can go from just bios on hardware and doesn't need additional bootloader? <gio>Hmm, I can reproduce your error. The integration of mm0 in asmc was only half-started, so I'm not surprised it doesn't work. It wouldn't do anything useful anyway. Basically, mm0 is a mathematical theory proof language, and the idea was to simultanously prove that asmc is correct and have a low level proof verifier that doesn't depend on loads of operating system and library layers. <gio>But I never finished it. <gio>I guess you should just disable it in asmg/main.g, so it doesn't get in your way. <gio>Disable the tests too, if you want to skip directly to the interesting part. <gio>(the tests are slow because the C compiler is rather stupid) <Melg8[m]>okay, i understand) so, what about "one thing that bothers me - i watched your presentation from 2019 - you said that bios -> bootloader -> than asmc - is that correct now? or you created image with mbr - and it can go from just bios on hardware and doesn't need additional bootloader?"? <gio>Melg8[m]: I am not sure I remember what I said in 2019, but for sure at some point I used to use Grub as bootloader. Now I don't any more, but there is still a custom bootloader in boot/. It's very small, so it's not a huge stretch to just consider it in the trusted seed. <gio>Though for the precise architecture check out the Makefile and the .gitlab-ci.yml files, so you can figure it for yourself. <Melg8[m]>okay, do you know any successors of your project? and your repo is on hold/abandoned/archived? <Melg8[m]>@gio and i want to ask, why you choosed to use ipxe and load kernel from the net? what were reason behind it? how hard it would be to change project to load kernel (and all other needed sources) from initial system (which forms "build" folder.) and build in air gaped isolated system without net? what main problems would be? <gio>Melg8[m]: I am not aware of anybody having taken over from my project, or even tried to do anything similar. Asmc is still fully on my todo list, though my todo list is very busy place, so asmc hasn't received basically any time slot in two years. <Melg8[m]>[[[[][[]][]][[][][][[]][[[]][][[][]][][][]]][][[][]][[][][][[][][[]][[]][[][][]]]][][[][][][][[]][][]][[][][][ <gio>I can't see that happening shortly, but I hope I will eventually find some time for it. <gio>I can give no ETA for the moment, though. <gio>At some point I even considered asking a grant to spend some time on it, but that required time too, and I didn't proceed. <gio>But, at least in my heart, it's not abandoned or archived. <gio>Everything you say is conceptually doable and probably even easy. Consider that for me asmc is a research/experimenting project, so there are a lot half-baked things and no choice is meant to be set in stone. <gio>I worked in iPXE because it seems a nice way to test what asmc could do; easier than Linux, but not trivial to boot, and I am happy with the result. Whether it will be a useful step in the long run or not, it will be seen. <gio>I am quite convinced that Linux itself should not be too hard to boot, but I've been saying this for years and never done it, so feel free to not believe me. <Melg8[m]>@gio i'm really excited that i found your project, don't know if my programming skills would be enough to add something useful to it, but at least as giant tutorial in baremetal bootstrapping - it looks like small miracle to me) you've done pretty good job) <gio>Also for tinycc, I tried this way to compile it with softfloat, but in retrospective I am not sure it is the best idea. Maybe it's more sensible to use the incremental approach like, I believe, they're doing with mes. <gio>Melg8[m]: Thanks! BTW, I learn a lot of stuff doing it, and hopefully the code is simple enough that it is worthwile to study it for you to learn something. <Melg8[m]>@gio did you manually ported M2-Planet to G? <gio>But don't take anything in it as a gold standard, there is plenty of stuff I'd like to see rewritten, starting for that awful C preprocessor you mentioned before. <gio>Melg8[m]: Yes. But porting from C to G is not hard, as soon as you get used to it. G is really designed to be a simpler C (simpler for the compiler, not for the programmer). <Melg8[m]>from one point of view - yea. for me G is much nicer to look at, than assembler - (i mostly programmed with C++) - but G - lacks infrastructure for it, and C has plenty (static analysis tools/compilers/etc) and M2 planet now have at least few active developer as from what i seen in this channel. So one logical (at least for me) thing would be to update M2 to never version and port back your G code to more C-like code - compiled with M2 <gio>Well, the only point of G is to get you a programming language when you have none. If you already have C, you would never even write anything in G, of course. <gio>So there is no point in porting stuff from G to C. <gio>And the only program that it is sensible to write in G is a C compiler, or a compiler for any more reasonable language. <gio>While it can be made better, it already exists, so in a sense every program that it makes sense to write in G had already been written. <gio>Now the remaining work to be done on asmc is basically in C. <Melg8>but it said in log 404 on this file (so request at least was performed and handled) <gio>A couple of years ago I ported M2-Planet to G to have a C compiler when I didn't have one, but now I do have, and I like my C compiler more than M2-Planet, so I don't have any reason to keep M2-Planet updated. <gio>Melg8: Did you start the server in the http/ subdirectory? <Melg8>@gio what differs your C compiler form M2-Planet? and why you prefer G->C compiler? except from familiarity point of view <gio>Though keep in mind that asmc essentially finishes there. <Melg8>@gio ... okay) i see)) now, i didn't) <gio>There is some code for booting Linux, but it's experimental and won't work. <gio>Melg8: First, notice that I am comparing my compiler with M2-Planet how it was a couple of years ago, I don't know how it has evolved now, my knowledge of it could be outdatesd. <gio>With this caveat in mind, I found M2-Planet code rather hard to read. Given that the purpose of such a compiler is to convince myself that it is correctly translating C to machine code without leaving windows for malicious stuff, it didn't really fill this expectation. <gio>From my point of view, my compiler is much cleaner, though not bug-free. <gio>It correctly parses and implements C types, while M2-Planet does not (or, at least, did not when I looked at it). <gio>Also, I don't like the macro language that M2-Planet uses for the assembling stage. I don't think a macro language is appropriate for replacing a real assembler language. <Melg8>it would be interesting to do DDC on G-C and M2-Planet compilers) <Melg8>we have to implementation of C compiler - from assembler directly cc_ and from G - and have M2-planet source code which is C code - so we can check what would be result of building cc_ -> M2 ->M2 vs G -> M2 -> M2 . they should have same hashes <gio>Also, my compiler properly implements some more specific C rules, like integer promotion, type promotion, anonymous structs (I think I remember), initializers. <gio>Ah, yes, I remember. <gio>In asmc you can modify http/continue.c and asmc will basically compile it and run it, you can put in there whatever you want. <gio>(as long as tinycc can handle it) <gio>Though now I have to go. Good day! <Melg8>@gio thanks alot for your time! <mitzman>i thought of it as being more guix-related. ^^ <mitzman>but somehow my situation keeps getting more interesting. i see that gcc-mesboot1 is built with glibc-mesboot0. the glibc is built with --disable-shared, while gcc-mesboot1 requires a dynamic linker, but can't find ld-linux. glibc was supposed to create the ld-linux anyway? <siraben>xentrac: why on his death (June 7) instead of (June 23) <stikonas>Melg8: yes, that value when building tcc is dummy <stikonas>tcc was unable to compile things required for dynamic loader <xentrac>siraben: i think it's especially important to remember the tragic circumstances of his death