IRC channel logs

<stikonas>hmm, actually doing it from GCC 4.0.4 might be easier...

<fossy>stikonas[m]: sure

<fossy>stikonas[m]: do you have any thoughts on changing /image to /usr. This is because when I attempt to migrate to a "real" FHS filesystem structure we would have to rebuild many things cause /image is hardcoded...

<stikonas[m]>fossy: I tried use before image, it didn't work

<fossy>huh, why not?

<stikonas[m]>Possibly due to some fix includes stuff...

<stikonas[m]>Didn't investigate more, but it was non trivial

<fossy>hm, I'll give it a try. If not then I guess we will have to rebuild

<stikonas[m]>Rebuild might hit the same problem

<fossy>possibly.. what package/software wouldn't like existing in /usr though

<stikonas[m]>Hmm, it was probably GCC pass2

<stikonas[m]>That failed

<fossy>hm ok

<stikonas[m]>So something on build system treats usr in a special way

<stikonas[m]>Maybe it's fixable with more work

<stikonas[m]>But yes,I would prefer /usr too

<fossy>pushed a fix to kaem for PATH variable... explains the earlier hacks we had to do lol

<siraben>NieDzejkob: oh you are also in formal verification (saw you at proof ground 2021)

<fossy>interesting, tcc compile seems a bit slower with mes-m2... wonder why, given that we were using mes compiled by m2-planet before

<siraben>into*

<siraben>I did a little experiment recently, verifying factorial for a simple assembly language https://gist.github.com/siraben/cb58432b9cd755e80c548de40e5fe867

<fossy>what is proof ground

<siraben>The program is `[JZ 7; ST C; MUL ACC; ST ACC; LD C; DEC; J 0; LD ACC; HALT]`

<siraben>fossy: think competitive programming but for theorem proving

<siraben> https://www21.in.tum.de/~wimmers/proofground/

<siraben>basically you're given a question and have to formally verify it

<siraben>like a SAT solver or some data structure

<fossy>right

<fossy>kinda cool

<siraben>Of course it requires both being able to be good at proving in general then translating it to one's proof assistant

<fossy>what are you using there?

<fossy>in that gist

<siraben>I think proof writing is like programming, with enough practice it becomes natural.

<siraben>fossy: Coq.

<siraben>NieDzejkob uses Isabelle IIRC

<fossy>ahha

<siraben>The key correctness lemma is `Lemma fact_n (n : nat) : { m : store | csteps fact_prog (0, n, set empty ACC 1) (8, fact n, m) }.`

<siraben>to translate what this means;

<siraben>it says for every natural number `n`, there is a store `m` such that the factorial program steps from the initial state where PC = 0, A (the only register) = n, mem = empty[ACC] = 1 to the final state where PC = 8, A = fact n, mem = m

<fossy>zzzzzz

<fossy>oops

<fossy>stuck key

<siraben>lol thought you fell asleep

<siraben>anyway that was a pleasant start that took me a few hours yesterday, I'm contemplating proving a stack data structure correct in assembly

<siraben>so I would need to relate the abstract representation of the stack as a Coq list of natural numbers with the in-memory representation

<siraben>and show that the abstract representation changes as expected when I push/pop

<NieDzejkob>siraben: haha, yeah. small world

***stikonas_ is now known as stikonas

IRC channel logs

2021-07-06.log