<dylex>
Not sure if this is the right place to ask, but I'm trying to find the right way, in an overlay, to patch qt510.qtbase. I'm trying qt510.overrideScope (super: self: { qtbase = super.qtbase.overrideAttrs ... }) but it doesn't get picked up by other qt modules.
ashgillman has quit [Ping timeout: 260 seconds]
ashgillman has joined #nixos-dev
disasm has quit [Quit: WeeChat 2.0]
ma27 has quit [Ping timeout: 256 seconds]
ashgillman has quit [Ping timeout: 264 seconds]
disasm has joined #nixos-dev
<gchristensen>
error: executing SQLite statement ‘delete from ValidPaths where path = ?;’: database or disk is full (in ‘/nix/var/nix/db/db.sqlite’) hehe
ma27 has joined #nixos-dev
<shlevy>
womp womp
<shlevy>
pbogdan: No idea :(
<shlevy>
Through some quirk of scheduling my glibc-2.27 branch is turning into a "fix all the /bin/sh impurities" branch
mbrgm has quit [Ping timeout: 265 seconds]
mbrgm has joined #nixos-dev
ma27 has quit [Ping timeout: 246 seconds]
lopsided98 has quit [Remote host closed the connection]
garbas has quit [Ping timeout: 245 seconds]
garbas has joined #nixos-dev
<angerman>
Has anything wrt to —cores 0 changed with nix2?
<angerman>
I have a funny feeling that it parallizes less aggressive...
<clever>
angerman: ive noticed that it does both -j and -l, so make checks the loadvg
<clever>
and it tends to only do 1 job at once until the loadavg drops, then it spawns a ton of jobs
<angerman>
clever: It seemed to have been more aggressive. I think it used to be 100% utilization all the time. Now it's more like some oscilating utilization. But I might misremember, don't have data to back that up.
lopsided98 has joined #nixos-dev
<clever>
angerman: if you watch the loadavg in `top`, does it hover around your core count?
<angerman>
clever: hmm tried to build something else, now it's all 100% again... maybe there was some sequential dependency in there I did not expect.
<angerman>
Anyone seen this: `ln: failed to create symbolic link './links': File exists`?
GlennS has quit [Quit: No Ping reply in 180 seconds.]
orivej has quit [Read error: Connection reset by peer]
orivej has joined #nixos-dev
GlennS has joined #nixos-dev
orivej has quit [Ping timeout: 260 seconds]
davidlt_ has joined #nixos-dev
davidlt has quit [Ping timeout: 265 seconds]
Jackneillll has joined #nixos-dev
Jackneilll has quit [Ping timeout: 240 seconds]
<angerman>
ahh...
<Mic92>
over 900!
orivej has joined #nixos-dev
orivej has quit [Ping timeout: 256 seconds]
ma27 has joined #nixos-dev
pxc has quit [Ping timeout: 265 seconds]
davidlt has joined #nixos-dev
davidlt_ has quit [Ping timeout: 256 seconds]
davidlt_ has joined #nixos-dev
davidlt has quit [Ping timeout: 264 seconds]
Lisanna has quit [Quit: Lisanna]
orivej has joined #nixos-dev
FRidh has joined #nixos-dev
<Profpatsch>
grahamc: Prepare for PR impact!
<gchristensen>
??
<gchristensen>
merging or opening? :P
obadz has quit [Ping timeout: 246 seconds]
<MichaelRaskin>
Maybe both?
obadz has joined #nixos-dev
<Profpatsch>
gchristensen: opening. The rewrite of meta typecheck logic.
<gchristensen>
ohh
<Profpatsch>
gchristensen: How do I reevaluate all packages to see whether it finds meta type errors?
<Profpatsch>
A diff for that would be nice to have, stretch goal. :)
<Profpatsch>
For reference, the full maintainers type description looks like this:
<Profpatsch>
should be: { [available: boolean], [branch: string], [broken: boolean], [description: string], [downloadPage: string], [downloadURLRegexp: string], [executables: list of string], [homepage: one of [ list of string, string ]], [hydraPlatforms: list of string], [isBuildPythonPackage: list of string], [isFcitxEngine: boolean], [isGutenprint: boolean], [isIbusEngine: boolean], [knownVulnerabilities: list of
<Profpatsch>
string], [license: one of [ list of string, attrset of string, list of attrset of string, string ]], [longDescription: string], [maintainers: list of { email: string, name: string, [github: string] }], [name: string], [outputsToInstall: list of string], [platforms: list of string], [position: string], [priority: integer], [repositories: attrset of string], [schedulingPriority: integer], [tag: string],
<Profpatsch>
shlevy: Hm, I’m not sure if that’s such a bad thing.
<Profpatsch>
GHC is already >1 GB unpacked.
<shlevy>
I think it's probably the right choice for now
<shlevy>
It just says something unfortunate about the overall ecosystem
<Profpatsch>
And we already had to manually statically link every binary anyway, because of the RPATH startup time issue
<shlevy>
That we can't split out base libs easily, that dynamic loading is so damn slow, that we can't optimize and share code...
<Profpatsch>
e.g. purescript takes 4+s to start, just stating (160^2)/2 = 12800 files.
<shlevy>
Yeah
<shlevy>
We should write our own dynamic loader :P
<Profpatsch>
Well, setting absolute so-paths for every nixpkgs exectuable is long overdue.
<Profpatsch>
IIRC sphalerite was working on it sometime last year.
<Profpatsch>
He had a pretty good idea how to achieve that.
<shlevy>
Wait ELF already supports that?
<shlevy>
Ugh why are we mucking about with rpaths and crap?
<Profpatsch>
yeah, exactly.
<gchristensen>
I think abbradar was working on that?
<gchristensen>
if I had to guess, we're doing it the current way because nobody has spent the time to do it the other way :)
<shlevy>
gchristensen: Of course :D Just surprised that this is an option
<gchristensen>
yeah, I think it is sort of lore... a few times now someone has learned this is possible :D
<Dezgeg>
I think ELF doesn't support it cleanly
<Dezgeg>
only in different shades of hacks
<sphalerite>
yes I was
<Profpatsch>
Dezgeg: If you set an absolute path, ld.so will do exactly one stat.
<Profpatsch>
And not look into RPATH.
<sphalerite>
yeah it does support it cleanly
<Dezgeg>
yes, but doesn't that potentially break other stuff
<sphalerite>
you still need RPATH for dynamically loaded stuff IIRC
<Profpatsch>
But the idea was to do it the other way around, I forgot how it works.
<sphalerite>
but the issues I was running into were spurious crashes very early on in program execution
<Dezgeg>
yep, dlopen() was one of the things I was thinking of
<sphalerite>
I lack the low-level wizardry to understand what exactly was going on there
<sphalerite>
but my best guess is it's a patchelf bug
<Profpatsch>
I think setting the library names to the full path instead.
<Dezgeg>
what happens then if two versions of different libraries are attempted to be loaded?
<Profpatsch>
Yeah, we had a patchelf bug iirc.
<Profpatsch>
Dezgeg: dlopen() has to patched in the source anyway.
<Dezgeg>
no
<Profpatsch>
Or should at least.
<Dezgeg>
if say libz is in RPATH, then dlopen("libz.so.1") without an absolute path will work
<Dezgeg>
honestly, I start to think the easiest way is to read the directories with readdir() and make a cache
<Profpatsch>
Now you have a correctness problem and a cache. :)
<sphalerite>
ld.so.cache per executable, generated at derivation build time :D
<gchristensen>
better than a zillion stat calls maybe
FRidh has quit [Quit: Konversation terminated!]
<Dezgeg>
well, nix store directories are immutable so no real chances of coherency problems
davidlt_ has joined #nixos-dev
<shlevy>
So not that this would fix the real issue, but why does ld.so stat instead of just opening anyway?
<sphalerite>
maybe it's faster?
<shlevy>
But it needs to open all the libs eventually right?
<Profpatsch>
shlevy: You have exactly one .so per RPATH entry.
<gchristensen>
well it is stat'ing looking for the presense of a file
<shlevy>
Right
<shlevy>
You can look for the presence with open just as well
<Profpatsch>
So you get a quadratic explosion of stats.
<shlevy>
Sure, I get that open won't fix the real problem
<Profpatsch>
Or syscalls in general.
<shlevy>
I'm just wondering why it's stat at all
<Profpatsch>
shlevy: Maybe open calls stat?
davidlt has quit [Ping timeout: 256 seconds]
<shlevy>
Nope
<Profpatsch>
I don’t know, why does autotools do 20000 checks at the beginning of each build? :)
<shlevy>
:D
<shlevy>
Portability
<shlevy>
These days though autotools should just give you a target-specific pre-compiled binary :P
<sorear>
do you open and then stat or do you stat and then open? does it make a difference?
<Dezgeg>
apparently the st_dev + st_ino combo is used for... something
<gchristensen>
I'm guessing the reason it probes with stat is so it doesn't look at all the files in the monster /lib dirs most distros have
<shlevy>
sorear: Why do you need to stat at all? And I think open + fstat is better than stat + open anyway
<shlevy>
It's only if they're looking at something besides !ENOENT
<shlevy>
to decide whether to open
<Dezgeg>
to detect duplicates for some reason
<shlevy>
if it makes sense
<gchristensen>
what if we patched it to list the directory instead of their blind probes?
<gchristensen>
since we don't have monster lib dirs
<shlevy>
stat will be faster than readdir for sure
<shlevy>
Unless they read all the dirs at once
<shlevy>
and reuse the list
<gchristensen>
will readdir once on each rpath vs. the combin...yeah that
<shlevy>
I'm sure someone somewhere has written a DSO that at load time makes another DSO in the rpath :P
* gchristensen
knows what some of those words means
<gchristensen>
shlevy: what is the implication of that?
<shlevy>
Dynamic libs can have code run immediately at load time (this is how e.g. static C++ ctors are called). It's possible that initial load is different from dlopen, but if not someone could have a library liba.so that creates libb.so in the same directory at load time, thus satisfying a later libb.so call in a way that your read-dirs-once approach wouldn't
<shlevy>
Of course that wouldn't work in the Nix world
<shlevy>
But I bet someone has actually done something like that and I'm not sure if glibc would consider that valid or not :D
<gchristensen>
my god
<Dezgeg>
I really anybody would do that with a non-absolute path
<Dezgeg>
given that you need to be root
<shlevy>
True
* shlevy
imagines rewriting the RPATH entry of the loaded binary in memory
JosW has joined #nixos-dev
<clever>
shlevy: something i thought about, is that global pointers in the program itself are initialized after dynlib loading, but before main() is called
<gchristensen>
can you count on such a heinous person to care about needing root? ?:)
<shlevy>
I doubt that would work but it'd be fun tot ry
<clever>
shlevy: and a dlopen()'d library may refer to the globals of its parent program
<clever>
but if you inject it into DT_NEEDED, it runs too early
<Dezgeg>
well, actually you could just modify LD_LIBRARY_PATH
<shlevy>
clever: Yeah, it may be the case that __attribute__((constructor)) is deferred until after the NEEDEDs are loaded
<clever>
i was thinking about how to trick --shrink-rpath into detecting the library
<shlevy>
I haven't actually tried
<Dezgeg>
but I think this is getting into too theoretical territory :)
<shlevy>
MichaelRaskin: I'm really happy about your latest email to nix-devel as that's basically exactly how I've been thinking about things :D
<MichaelRaskin>
shlevy: I am not completely sure if I have given up on getting this done from the ground up before you have joined the Nix land…
<MichaelRaskin>
But there has been enough drift over the years, so maybe now there is a chance
<shlevy>
Yeah. Especially if we're talking about language changes.
<gchristensen>
shlevy: ping me next time you see the macs doing the wrong thing btw
<shlevy>
gchristensen: OK, will do, thanks!
<MichaelRaskin>
Why do I get that feeling that getting anything done right will practically require compiling parts of Nix-written core library to an .so ?
<gchristensen>
hopefully they're all "fixed" now
<shlevy>
MichaelRaskin: Luckily we have a really good package manager to use if we need that;)
<gchristensen>
!m nix
<MichaelRaskin>
I have a feeling that it will make sense to have that in ~/.cache and not in packaging
<MichaelRaskin>
Because otherwise juggling branches will be more complicated
<shlevy>
Sure, but could still be a nix derivation to actually build it
<shlevy>
I also think separting out nixpkgs library from nixpkgs package set may eventually make sense
<MichaelRaskin>
…and there you go with mandatory builds during eval
<shlevy>
:) it's morally just evaluation
<shlevy>
It wouldn't be anormal nixpkgs derivation. All dependencies would have to be self-contianed in Nix if we went that route (possibly through a new kind of "builtin" derivation like fetchurl)
<MichaelRaskin>
Just make sure you don't need compiled stdenv to compile stdenv
<MichaelRaskin>
Full speed to gridlock where everyone is afraid to change anything, because it would break this or that really cool n+1-th order tool
<shlevy>
Formal specs or bust
<gchristensen>
ofborg has no spec and any compatibility is incidental
<MichaelRaskin>
shlevy: they give you nothing for negotiating actual external changes
<gchristensen>
ofborg can worry about external tooling when the work is paid for :P
<shlevy>
I mean specs for the interface :) I'm being facetious but IMO if you have a well-defined interface you can break everything outside of it with impunity, Linus-be-damned
<MichaelRaskin>
shlevy: the problem is that ofborg is in the state where it does want o break external interface
<shlevy>
Sure. So it doesn't have one at all ;)
<MichaelRaskin>
And also I think I can realistically lie with a spec just as well as with statistics
<gchristensen>
I mean shoot, sometimes I even break the log viewer
<gchristensen>
nothing is sacred
<gchristensen>
gotta move forward
<shlevy>
MichaelRaskin: Sure, I'm assuming some level of good faith :P
<gchristensen>
only so many hours in the day
<shlevy>
I do think if we move to branch protection then that does legitimately constrain you somewhat :)
<gchristensen>
only on core functionality, which I do obviously want to keep working
<shlevy>
Yeah
<MichaelRaskin>
shlevy: I have an experience that many formal spec advocates don't have. I taught formal logic to students, and decided that it is a good idea to tell about computer methods (everything was in the first-order, so first order automated provers were the specific technical thing to look at). I asked them to encode some trivial algebraic statements and let the prover prove them, then I looked carefully at the proof graph, explained the mistakes and
<MichaelRaskin>
Look, I know these students, it was not bad faith, you can lie with a spec and not even notice.
<shlevy>
Hmm can you give examples? I mean I know mistakes can happen but I'm curious if this is a "forgetting to do using namespace std or std::cout" kind of mistake or "buffer overrun in C" kind of mistake?
<MichaelRaskin>
The second, because the proof worked!
<MichaelRaskin>
Strictly worked, it's just the statement that was trivial.
<shlevy>
I meant more in terms of how likely an experienced programmer is to hit it :)
<shlevy>
Anyway, of course specs themselves need careful review and can be wrong
<shlevy>
I'm not suggesting they are any kind of panacea
<MichaelRaskin>
Depends on the size of spec and quality of automation. Maybe unlikely with Coq because it is not smart enough and requires you to do enough grunt work to notice.
<gchristensen>
also I'm not going to write one, so
<shlevy>
:o
<shlevy>
:D
<shlevy>
If/when formal methods get more of a foothold in engineering, I suspect we'll reach a point where specs that are too big to fit into your head are considered inherently buggy and in need of modularization
<MichaelRaskin>
shlevy: oif course, the mistakes in the spec the students made were simple ones, because the property to define was a trivial one.
<shlevy>
But anyway I do believe it's in principle a much easier task to human-verify a spec than to human-verify an implementation
<MichaelRaskin>
Formal methods need to come back and remember the great truth of Gödel's completeness theorem first.
<MichaelRaskin>
(although, as my experiment shows, that is not enough)
<sorear>
the axioms of first-order logic are sufficient to derive a contraction in all theories for which a model does not exist?
<sorear>
*contradiction
<MichaelRaskin>
Yes.
<MichaelRaskin>
Speaking of formal specs, though, I should probably write that one email I wanted to write to the design-goal discussion, but decided to avoid.
<MichaelRaskin>
Let's let people decide whether to ignore it…
<MichaelRaskin>
Right, also an example of a problem uncatchable by formal spec — of course the spec would be «everything succeeds»
<MichaelRaskin>
Well, you would get a second chance to roll for perception on the «and not empty» clause
<gchristensen>
it is funny because that ... shouldn't happen
<gchristensen>
-A tests.foo -> error: attribute 'foo' in selection path 'tests.foo' not found
<gchristensen>
so a definitetly fun edge case
<MichaelRaskin>
Maybe the attributes exist but are empty sets?
<MichaelRaskin>
Or non-derivation-containing sets.
<shlevy>
I find this a bit of an unfair response that comes up whenver anyone mentions formal methods. Very few people, if any, claim it would make truly bug free code, or that you shouldn't also use tests and code review and all the other tools available
<shlevy>
The question is not whether it's perfect, but whether it can be brought to the point where the benefits outweigh the costs (I don't think we're there now)
<sorear>
are you responding to something outside the channel?
<shlevy>
MichaelRaskin's "a problem uncatchable by formal spec" :)
<shlevy>
No one would say that if the previous conversation was about how we need more tests
dylex has left #nixos-dev [#nixos-dev]
<MichaelRaskin>
shlevy: well, notice that I did say that writing that spec would give you a second chance to think of it, even though it won't guarantee
<shlevy>
Sure, it's more of a general annoyance than anything about your point in particular
<shlevy>
I don't think this is specific to formal methods... Any significant enough departure from the status quo is expected to solve all problems or be considered worthless
<MichaelRaskin>
Every significant enough departure from the status quo is first done wrong, though. And I am sincerely not sure that formal methods have already passed that part. (My point about completeness theorem was a bit about the fact that I hope that people find a good way to express things in first-order logics — where we have powerful tools and good textbooks even for good high-school studentes)
<shlevy>
I'd really like better systems that constrain you to simpler/saner logics by default but let you break out (with more manual work) if necessary
<shlevy>
I know coq has tactics for e.g. first order logic but it's not quite the same
<MichaelRaskin>
Are you sure it is better to use logics above FOL, and not axiom sets?
<shlevy>
No, I'm not
<shlevy>
But a system such as I just wished for would let you compare both, no?
<shlevy>
While reusing a common base
<sorear>
for some reason set theory and classical logic are passé
<MichaelRaskin>
Too bad QED seems to fizzle out.
<shlevy>
sorear: I think there is a strange fetishization of program extraction
<sorear>
fol+zfc is far more powerful in the godel sense than most of the modern systems
<MichaelRaskin>
After learning quite a bit of model-theory-of-set-theory, I would say that my ideal hope would be a first-order-logic based structure theory with better tradeoffs
<MichaelRaskin>
sorear: not always a good thing, though
<shlevy>
I actually like to stay constructive when possible, but I don't think it's fundamental to the kinds of proofs that make sense in software verification
<shlevy>
MichaelRaskin: Any reading you recommend to get a sense of what that would look like?
<MichaelRaskin>
For staying constructive there are some FOL-on-intuitionism approaches that are nice but not fashionable
<sorear>
MichaelRaskin: I was replying to 'Are you sure it is better to use logics above FOL' - logics actually above FOL are very rare, most logics are below it
<MichaelRaskin>
We-ell
<MichaelRaskin>
sorear: they are often sideways from it
<MichaelRaskin>
People include as inference rules what would be axioms when building on FOL
<MichaelRaskin>
The separation stops being the same and it is hard to compare…
<MichaelRaskin>
shlevy: not likely to be a good direction, but a different enough direction to believe in diversity is NF
<shlevy>
NF?
<MichaelRaskin>
(New Foundations; intorduced by Quine in the middle of the twentieth century)
<MichaelRaskin>
Not so new anymore but still called NF…
<shlevy>
This is why you never put "new" or "ng" or any such thing in your name :P
<MichaelRaskin>
There are no good newer ones anyway!
<MichaelRaskin>
I would compare NF and ZFC like that: {X|¬X∈X} is a contradiction and it needs to be forbidden. ZFC says that it will be too large to be a set (and it happens to coincide with the class of all sets in NBG extension of ZFC); NF says that it checks if X is in X, which is a rampant layering violation, and therefore too complicated to be guaranteed to exist (and it doesn't exist, because its existence is a contradiction)
<MichaelRaskin>
In a way NF is a way of bringing together the simple forms of type theory and the FOL.
<MichaelRaskin>
(before opening — are, The page that collects all the nice links about NF?)
<sorear>
holmes has a bunch of links about NF, but I'm specifically referring to the consistency proof
<MichaelRaskin>
Oh, a fresh rewrite of the proof.
<sorear>
well you might not have seen any version of it
<MichaelRaskin>
I haven't read any version of the proof, that's true.
<sorear>
I have, but not long enough to be fully convinced
<MichaelRaskin>
Last when I checked he posted an early draft with the intention to revise a lot, and I didn't keep track to pick a moment when it is ready for reading.
<MichaelRaskin>
Is it for NF or NFU?
<MichaelRaskin>
Ah I see
<sorear>
Consistency of NFU has been settled since 1960s, NF is new
<MichaelRaskin>
sorear: for NFU I never dived enough to see how much strength it has w.r.t. ZFC. Consistency proof is just one direction.
<Profpatsch>
gchristensen: Okay, I have elimintated a meta errors for now.
<gchristensen>
ok cool
<Profpatsch>
And I can even restrict license so that (list string) is gone.
<shlevy>
I've long wondered how much these foundational issues matter when you're not reasoning about the system itself. e.g. if you disabled universe checking in coq and were just trying to prove things about programs in a deep embedding of some other language how likely are you to accidentally prove something false?
<gchristensen>
I think the right thing here is to recurse in to the attrs but don't want to manipulate the input from the command because it is a bit less safe