***jxself is now known as Guest41915
***JamesJRH_ is now known as JamesJRH
<DusXMT>Sent my favorite PDF reader to ML <Tsyesika>YES found my usb drive, now i can boot guix :D <DusXMT>psst.. the os is actually called gnu. <civodul>jxself, mark_weaver: BTW, the "rmmod snd_hda_intel && modprobe snd_hda_codec_analog && modprobe snd_hda_intel" trick does indeed work for me <civodul>well it works now, but my attempts a couple of days ago failed, for some reason <philed>civodul: I fixed my problem with "guix pull" in the end, by looking at IRC logs you'd participated in. :) I needed to create ".config" in /root <civodul>so you were eventually able to reconfigure, right? <civodul>if you've accumulated a pile of bugs, don't hesitate to mail them ;-) <philed>So to confirm, %base-file-systems is only defined in guix 0.7, and I hadn't been able to pull this because I was missing .config. Now it's all fine. <DusXMT>I think the .config/guix cirectory creation should be noted in the documentation somewhere, as every single person stumbles upon it <civodul>i think it should just work out of the box <philed>Hey civodul, do you know any of the Coq folk? <civodul>i've met people involved with it in the past <philed>Just my biased perspective means I always think Coq when I hear INRIA. :) <philed>I haven't used it myself, but I'm in the theorem proving community. <civodul>before coming to Inria, what it meant to me was OCaml + Coq + Bigloo <civodul>philed: do you work with Isabelle, or Agda, or something else? <philed>HOL Light, but we're currently writing our own web-based prover. <philed>From scratch. We think it needs to be web-centric from the ground up. But I'm currently working to transpile all of HOL Light into it, as a bootstrap. <civodul>there are lots of things to dislike about the web, but at least it allows language people to pursue interesting work <Svetlana>Web-centric apps might be a bit hard to make scriptable in languages different from javascript. and javascript only changes stuff clientside <philed>civodul: That's got my curiosity. What do you dislike about the web? (not saying I don't have plenty of my own dislikes :) ) <philed>Svetlana: We've had the audacity to invent another scripting language, this one supposedly tailored to theorem proving. Personally, I wanted to just go with scheme and some choice macros. <Svetlana>trust me, learning new languages is hard and the idea to have all software scriptable in a single language has solid ground <Svetlana>I'm raging at a lot of software that's not only not scriptable properly, but is scriptable in js (clientside) and in php (serverside) which forces me to learn 2 languages to actually do a single thing <Svetlana>On the plus side, both the 'frontend' and the 'backend' would be on the user's computer, which makes things a bit easier. But having to keep learning is pretty hard. <philed>civodul: Otherwise, we're hoping that theorem proving is a unique point in the space of collaboration. You can state the problems you need solved unambiguously, and you don't have to human-check the solutions. The theorem prover is going to be a single indefinitely running runtime, and we hope that'll give us great opportunities to distribute problems and reintegrate solutions. <civodul>what i dislike about the "web apps" trend is that it's most often about taking control away from users <philed>Svetlana: Yeah, it's horrible. I'm not expecting it to last for long, though. <Svetlana>civodul: quite. The control goes away when someone /central/ hosts it though. When you have the entire thing on your machine, it's a little easier. <civodul>technically it's also easier to provide a specific server+client, than to devise a generic protocol that others could implement <civodul>Svetlana: but once you have the entire thing on your machine, better use Guile and whatever GUI library you like :-) <civodul>(rather than a web server at localhost:80) <civodul>that being said, i like things like davexunit's guix-web <civodul>it provides a nice GUI, and some people will find it natural to just jump to the browser <civodul>ISTR that jgay was on this channel at some point? <philed>civodul: On that front, I think we're largely innocent. We want the web to leverage distributed computing power and gather data for recommender systems to help advise users how to solve their problem, and to provide a single stable runtime for people to work in. In theorem proving, with, say, HOL Light, you can be running the same REPL for weeks and just incrementally adding to it. We want a single REPL shared by all users. But the <philed>whole thing will be open source too, to run intranets for small theorem proving groups. <civodul>philed: sharing theorem proving experience like this sounds cool, indeed <DusXMT>I wonder, what for email is available on GNU? Any recommendations? <jxself>Don't people use Emacs for everything? <philed>jxself: What do you use for email in emacs? *DusXMT ain't an emacs user just yet. He likes the concept, and even tried diving in onve, but he drowned in the documentation and is back to vi. <jxself>I don't use Emacs, philed. Just trying to think of something GNUy. :) <jxself>Because Fetchmail+Procmail+Mutt makes for a good combo, IMO. <mark_weaver>civodul: I've been struggling with hydra. I'm trying to cancel all the jobs in the queue, since it's all for core-updates and that's going to have to be rebuilt from scratch anyway, but my attempts to do so seem to be ignored. <mark_weaver>also, my last attempt to evaluate core-updates was pending for hours and finally timed out. (just as well, since we have to fix the format warning thing) <mark_weaver>more generally, I'm rather discouraged by how long it's taking for us to implement security updates to glibc :-( <mark_weaver>(well, the first time I asked it to clear the queue, it _did_ cancel around 170 jobs or so. but there are many hundreds more that I'd like to cancel but can't seem to) <davexunit>civodul: jgay wants my help to do the free software directory + guix integration stuff he has in mind. :) <DusXMT>I've looked at FPC (The Free Pascal Compiler) as it's on the wishlist, and apparently, it itself is written in pascal, so there needs to be a bootstrapping pascal compiler of some sort before it can be compiled... hmm... <DusXMT>I personally think the easier route will be to use gpc (GNU Pascal Compiler) instead, but that only works on old versions of gcc (I think up to 4.1) <philed>davexunit: Thanks. I'll have a look. <jxself>dusxmt: Download the compiler binary from freepascal.org and use that to compiler the compiler source? :) <DusXMT>jxself: I guess that could work? .. that's what gentoo does, but I doubt I can do something like that just yet, I've barely scratched the surface of scheme yet. <mark_weaver>jxself: their binaries presumably won't run in the guix build environment, because our libraries, dynamic linker, sh, etc, are in non-standard places. <mark_weaver>there's also the question of which architectures they provide binaries for. <mark_weaver>jxself: still, I guess your suggestion is our only option for cases like this. <jxself>Unless someone has a better idea. <mark_weaver>I guess there's no way to get thompson viruses out of such compilers :-( <DusXMT>It would be interesting to see if gpc can compile fpc, and if that could work, we could build fpc by the gpc compiled compiler, and recompile fpc with that, getting a bootstrap binary which could then be used to build fpc for the user to use... But that assumes gpc can compile fpc, which I kind of doubt it can. <jxself>Or to at least detect it, I mean. <ijp>well, it still can't be detected without a trusted compiler of sorts, but it does lower the barrier <mark_weaver>yes, it is, but that requires the existence of multiple different compilers that are capable of bootstrapping the desired target compiler. <mark_weaver>so we can use that strategy on GCC, or at least versions of GCC that can be compiled with plain C. <ijp>the low barrier being "can bootstrap your compiler" which is often surprisingly high <mark_weaver>but if FPC can only be compiled by itself, I don't see how to apply David Wheeler's strategy here. <mark_weaver>GHC is another example of a compiler that can only be compiled by itself. <philed>Get GHC to compile itself to C, first, then you've got a portable GHC? <mark_weaver>yeah, but that C is not source code. it's not practical to audit it. <mark_weaver>i.e. the thompson virus would be hidden in that intermediate C code and we wouldn't be able to see it there. <ijp>(assuming for arguments sake that said virus hasn't bugged the tools you are viewing the source code) <ijp>the thompson bug is really every paranoid's wet dream :) <mark_weaver>heh, yeah, it's quite a rabbit hole when you think about it. <mark_weaver>it would be good to have a bootstrap strategy that doesn't require any previous object code at all, but it would be quite a project. <mark_weaver>but it practice, it would probably be sufficient to write a very simple C compiler, run it on a very old computer with an old copy of Debian, and use it to bootstrap the last version of GCC that was written in plain C. <mark_weaver>(crucially, keeping the computer disconnected from the network at all times) <ijp>and the developer, you never know... <mark_weaver>the idea being that any thompson virus present in the old Debian would not know about whatever C compiler you used to bootstrap. <mark_weaver>and that by keeping the computer isolated, one can make assumptions that the intelligence of its thompson virus would be quite limited. *mark_weaver goes afk for a while <jxself>AFK? To go make a suitable virus? :) <ijp>I even wrote it in guile <philed>mark_weaver: This sounds like a cool concept. But why do you need to audit the generated C of GHC when you can just audit GHC? <philed>If you trust the environment in which you compile GHC to C, and you trust the GHC source, and you trust the C compiler on the target machine, everything should be well, right? <mark_weaver>philed: if there's a thompson virus in GHC, then it would presumably propagate itself to the generated C code. <ijp>philed: for your second compiler, it is assumed that it is not bugged. This is not the case with a C compiled version of ghc and a regular version of ghc <philed>mark_weaver: Yeah, but you audit the GHC code, right? <mark_weaver>philed: yes, but the actual conversion from GHC source code to C is done by a precompiled GHC binary. <ijp>philed: the problem of the thompson bug is that it is *not in the source code* but it is *in the executable* <mark_weaver>(and in this case, it would also be in the generated C source code, which is inscrutible and impractical to audit) <philed>Sorry, I'm probably thinking under different constraints. <philed>I'm pretty sure I understand the bug. <ijp>and any auditor that can find a thompson bug from the source will get burned as a witch *ijp grabs flaming pitchfork <philed>I was only half-reading the thread :) <mark_weaver>(it's not actually source code, even though it's in C) <jxself>I wonder if anyone's thought of this bug from a GPL compliance perspective. :) <jxself>The source code doesn't include the bug so it's not "complete and corresponding" as defined by the GPL. <ijp>bootstrapping is a weird area, because the GPL doesn't apply to the output of gpled programs <ijp>except for things like yacc <jxself>But if you're given a GCC binary containing this bug and then ask for the source code of said binary (which is your right under the GPL)... <jxself>The source code won't be complete & corresponding. <ijp>in any case, as with all compliance issues, the first thing you should do is contact the authors <ijp>doubly so here because it is a security vulnerability <mark_weaver>the word "complete" is not actually present in the GPLv3 <mark_weaver>The "Corresponding Source" for a work in object code form means all <mark_weaver>the source code needed to generate, install, and (for an executable <mark_weaver>work) run the object code and to modify the work, including scripts to <mark_weaver>control those activities. However, it does not include the work's <jxself>Yeah, I'm using terms of v2. They'd need to give the source code of the bug in order to be in compliance. <mark_weaver>System Libraries, or general-purpose tools or generally available free <mark_weaver>programs which are used unmodified in performing those activities but <ijp>bkuhn has probably considered this <jxself>Nah, an additional permission thing isn't needed because the modifications to GCC would fall under the GPL's terms already. <mark_weaver>It's an interesting idea, but I'm not sure what we could gain by investigating this further. If anyone put in a Thompson virus on purpose, I guess that violates laws other than copyright law. If they didn't put it in themselves, but were unwitting users of an infected copy of GCC, then I guess maybe the lack of warranty would protect them to some extent. <DusXMT>I think I'm going to put that exception I posted abive into my code, just as a fun easter egg <mark_weaver>I hope you don't put it into any code that might have future importance. <DusXMT>Really? I thought anyone can remove these exceptions and redistribute the work with the vanilla GPL license (of the appropriate version) <DusXMT>Or is that a different exception? I'm not sure, but I know one of them is removable <jxself>Yeah. "When you convey a copy of a covered work, you may at your option remove any additional permissions from that copy..."