lopsided98 has quit [Remote host closed the connection]
mfiano has left #nixos-chat ["WeeChat 2.0.1"]
lopsided98 has joined #nixos-chat
Lisanna has quit [Quit: Lisanna]
obadz has quit [Ping timeout: 246 seconds]
obadz has joined #nixos-chat
<gchristensen>
btw shlevy what were you doing w/ rust? :)
<shlevy>
gchristensen: looking at the merge-if-eval impl
<gchristensen>
cool
<gchristensen>
was your tweet about records related to rust feelings too? :)
<shlevy>
No, that was me possibly giving up on trying to shoehorn my ideas for next generation nix packaging into the existing language :D
<shlevy>
I want to see what systems have both records and sum types and how well they work
<shlevy>
(Haskell, for example, doesnot have good records but has excellent sum types)
<gchristensen>
oohh
<gchristensen>
gotcha
<MichaelRaskin>
In a sense, this is quite an old combination — both Pascal and C have it.
<gchristensen>
btw, the idea of "sum" types and "product" types reveals to me that I have nfc what "sum" and "product" mean at a fundamental level
<shlevy>
MichaelRaskin: Yes, in a very limited sense :P
<shlevy>
No row polymorphism, manual sum tags...
<MichaelRaskin>
Pascal does support a bit more machinery around sum tags, as far as I remember.
<shlevy>
gchristensen: Think + and x in set theory if you have that background
<MichaelRaskin>
gchristensen: sum and product are a _pair_ of associative operations, where sum is commutative and also there is a distributive law
<MichaelRaskin>
shlevy: in set theory you should use ∪ for +, if you are doing _just_ set theory.
<MichaelRaskin>
(Oh well, and I guess there are come cases where it almost makes sense to say ∩=+, ∪=×)
<shlevy>
:P
<shlevy>
Yeah
<gchristensen>
shlevy: I don't :( but I'll do some learning today
<MichaelRaskin>
Standalone, + is just a commutative associative operation, and × is just an associative operation
<shlevy>
Ah, if you don't then MichaelRaskin's approach is a better way to think of it
<gchristensen>
growing up I had my love for math stomped out of me one teacher accusing me of plagiarism at a time
<MichaelRaskin>
Using them together without a distributive law is Asking For Trouble™
<MichaelRaskin>
From a programmer's side I would recommend looking at min/+ matrix multiplication
<MichaelRaskin>
(where min is + and sum is × in terms of +/» pair)
<shlevy>
And type thoery I'd just look directly at sum type and product type. But it's better if you have a bit of the general sense of sum and product first
<MichaelRaskin>
It is something that makes sense algorithmically, and also really tries to beat the idea that «+» for numbers is addition
<gchristensen>
I have a practical understanding of what they mean, but not why those names are appropriatee
<gchristensen>
I'll do some reading after breakfast :)
<MichaelRaskin>
Well, if you look at the matrix multiplication algorithms, and min/plus matrix multiplication, you will see the structure of a +/× pair (which is enough for some of the algorithms)
<gchristensen>
ah ha! I get it
<shlevy>
Another way to see the appropriateness is look at how tupling morally distributes of unioning
<MichaelRaskin>
That requires already thinking in terms of a pair of operations with a distributive law, though
<MichaelRaskin>
So not so much another way, as the next step.
sorear has joined #nixos-chat
<MichaelRaskin>
So, of consistency of theories
<MichaelRaskin>
Well, in #nixos-dev we could make the side-by-side comparisons of types hard to read by intervening
<sorear>
If whatever correctness proof for a subset of nixpkgs you're working on turns out to require anything beyond PA this will be the most interesting metamathematical discovery of the 21c to date
<shlevy>
:D
<shlevy>
Who was that guy who was trying to demonstrate PA was inconsistent?
<MichaelRaskin>
It all depends on what programs you verify; if you are dependent on probabilities _and_ central limit theorem, you will distinguish a lot about set theories. As Solovay has shown, had the Analysis people been faster than Algebra people, we would have the self-evident axiom of Volume (every set inside a real cube has a volume) with different formalisations of many things
<MichaelRaskin>
Oh, many of them
<MichaelRaskin>
I think I know which you mean, though
<sorear>
the more I learn about the foundations of analysis the surer I am that the real numbers aren't
<shlevy>
:)
<MichaelRaskin>
Edward Nelson?
<shlevy>
Yes, that's him
<shlevy>
He passed away recently right?
<MichaelRaskin>
Not sure
<shlevy>
Yeah 2014
<MichaelRaskin>
Oh
<MichaelRaskin>
sorear: they are a useful abstraction to work with CLT which is useful to quantify risks
<MichaelRaskin>
But you can build them in very many different way
<MichaelRaskin>
Lebesgue measurability of everything + Directed-Countable-Choice for the win!
<sorear>
sure, they're useful
<MichaelRaskin>
Yesenin-Volpin did have a point about numerical existence, though.
<shlevy>
Surrounded by platonists! :o
<MichaelRaskin>
No!
<MichaelRaskin>
Yesenin-Volpin once said that 2^100 _doesn't_ exists
<MichaelRaskin>
doesn't exist
<shlevy>
But that implicitly concedes the framing of whether "numbers exist" is a meaningful statement
<MichaelRaskin>
When asked «But 1 does?», he answered «Yes». — And 2? — (after a small pause) Yes. — And 4? — (A second later) yes.
<shlevy>
:D
<MichaelRaskin>
Well, in the ultrafinitist approach it doesn't!
<shlevy>
There is definitely a distinction between 1, 2, 4 on the one hand and 2^100 on the other, but I don't think "existence" is the right one
<sorear>
2^100 is still smaller than the Eddington number, so to say that it doesn't exist is _rather weird_
<shlevy>
(though with 128 bit computers on the way that seems a low bound)
<MichaelRaskin>
sorear: in a way Eddington numnber is a real number, not a natural number. It is not the number of steps in any reasonable process, only an estimate of amount.
<MichaelRaskin>
(I do not completely support the position I am arguing, but then, I do not completely support _any_ position by now)
<MichaelRaskin>
shlevy: your initial question of «does it matter» has some intersection with QED manifesto
<MichaelRaskin>
I can also say that I have played with an automated theorem prover and an inconsistent naive set theory. A theorem is called simple if I do not lose patience before ATP succeeds, and the proof is independent of any contradiction. There are some simple theorems in set theory, yes.
<shlevy>
:D
<MichaelRaskin>
About your question about PA, though: if you want to prove termination of all the abstractions in Nixpkgs, it is really easy to start depending on a mid-sized ordinal.
<MichaelRaskin>
Of course, PA can work up to epsilon-0, so the fight for evaluation times might keep us from escaping PA, for now.
<shlevy>
I wonder how much would be lost if we replaced termination proofs with "if this terminates, it's correct" and "if it doesn't terminate or takes too long it doesn't matter, because someone will hit ^C"
<shlevy>
Maybe it's even easier to prove "this will or won't terminate within N steps"
<MichaelRaskin>
Actually, no
<MichaelRaskin>
Just as a trivial example, please answer two simple questions
<shlevy>
I don't mean in the general case
<sorear>
most interesting functions are primitive recursive or can be made so without anyone noticing the difference
<MichaelRaskin>
Integral from 0 to 1000 of x^10. Sum from 0 to 1000 of x^10.
<shlevy>
Just whether in cases that matter to program verification
<MichaelRaskin>
shlevy: note that my questions are _simpler_ than program verification
<MichaelRaskin>
Termination proofs of reasonable apptoaches tend to be simpler than polynomiality proofs. Then you ask about exact degree and the main coefficient, and enter the word of technical pain.
* sphalerite
needs to make a programming language where, by definition, any program that takes more than 1s to run on my laptop is invalid
<shlevy>
Anyway, my real point is that absent a specific notion of "fast enough" termination proofs need to be supplemented with performance testing, and if you're doing performance testing you'll catch non-termination anyway
<MichaelRaskin>
And of course, our fixpoint tricks are probably too powerful to be primitively recursive
<sphalerite>
that's an easy property to verify :D
<shlevy>
sphalerite: Not safely :D
<sphalerite>
who needs safety
<MichaelRaskin>
For example, this language doesn't have a correct interpreter
<sphalerite>
what about my laptop?
<sorear>
what happens if you get a new laptop? is this a temporal logic?
<MichaelRaskin>
What about programs that run for more or less than 1s depending on scheduling details?
<MichaelRaskin>
(Also, the disk caches wanted to say hi)
<sphalerite>
sorear: yes
<sphalerite>
MichaelRaskin: then they're correct or incorrect depending on scheduling details and disk caches :)
<MichaelRaskin>
I am not sure this definition of correctness is an improvement.
<sphalerite>
:D
<MichaelRaskin>
shlevy: of the general expectations with formal methods, I think there is also a lot of friction when someone tries to sell formal methods — especially with their current state — to the people who say «so, first you take a spec? wait, if I manage to extract a sane spec from the users upfront, the rest is easy!»
<MichaelRaskin>
Of course, then you suffer by association
<shlevy>
:D
<shlevy>
My domain is usually the systems world, where I think a proper spec is a bit easier :D
<MichaelRaskin>
Yeah, there correctness can actually be defined, Sometimes.
<shlevy>
A formal spec of "maximizes revenue" is possible, but very hard to prove
<MichaelRaskin>
In a non-profit you cannot even lie to yourself that this can ever become a formal spec.
<shlevy>
Maximizes global utility :D
<MichaelRaskin>
You just have some garbage that a counerparty — that you cannot get rid of because they are a government agency — mistakenly calls «data» and you want go chat with colleagues what interpretation of each line makes more sense and then you actually try to scale the decisions
<MichaelRaskin>
shlevy: I am not _that_ bad at game theory to miss the scaling problem for inter-subjective comparison of utilities.
<shlevy>
:D
<shlevy>
We should just skip to "solves my goals"
<MichaelRaskin>
As for «maximizes revenue» — I think some startups use it instead of something that would actually care about expenses
<shlevy>
Which of course may include "getting a big raise by making a lot of money" of course
<MichaelRaskin>
shlevy: «solves my goal» is back to «and if you can actually spec it in a way that can be verified by another person, I will do the rest»
<MichaelRaskin>
«maximizes the year's profit» sounds like a present for some round number of years since Marx birth, because it will maximise profit while landing the entire company in prison, most likely. Just as described in The Capital.
<MichaelRaskin>
I am not saying it cannot happen, though…
<MichaelRaskin>
«This is too stupid to happen is not a phrase one should say in 2018. Even more so, for a person speaking Russian…»
<MichaelRaskin>
Oops, the closing quote should be earlier
jtojnar2 has joined #nixos-chat
<obadz>
Don't want to distract you guys from debating socioeconomic theory, but I've been thinking the NixOS release model is a bit onerous as of late
<obadz>
Specifically since splitting out the security bug fixes from upgrades coming from upstreams is essentially impossible, pretty much all updates should go into the release
<obadz>
That means only big changes to nixpkgs are left out
<obadz>
Wouldn't it be better to have more feature branches and use staging more religiously to make sure master always builds, and have master be the rolling release?
neuralring has joined #nixos-chat
vdemeester` has joined #nixos-chat
<neuralring>
re: nixos-rebuild build-vm -- is there a default user/pass for logging into the vm instance or should hostUser login info work?
<MichaelRaskin>
neuralring: no idea, and it is a #nixos question for sure
<neuralring>
@MichaelRaskin, thx, will post there.
<obadz>
neuralring: I don't think so
<MichaelRaskin>
obadz: are you specifically asking in chat because of who will answer you here? I thought it is on-topic for -dev…
<MichaelRaskin>
When I update, I build from master, not even nixpkgs-unstable
<obadz>
MichaelRaskin: no, I just don't want to have that discussion with too big a circle especially as we're bug squashing 18.03
<MichaelRaskin>
I think nixos-unstable channel is what you want to have in master
<neuralring>
@obadz: thx
<MichaelRaskin>
I think -stable branch does make different choices in terms of «let a minor bug slide» vs «upgrade», and «use the upstream stable branch» vs «upgrade to newest»
<obadz>
on the former maybe, on the latter, I don't think so
<MichaelRaskin>
Of course the latter is only relevant when upstream does provide multiple branches with bugfixes, but this is probably so for server software
<obadz>
master doesn't default to unstable upstream software
<obadz>
not anymore than stable
<obadz>
I could simply switch to master without having the discussion, but my worries are:
<MichaelRaskin>
I think if there is an upstream normal release, and a bugfix for the previous release, -stable gets the latter
<obadz>
1) lots of nixos resources are devoted to stable: most importantly a lot of people's time. Hydra also prioritizes building stable.
<obadz>
2) When I was on master, it would often go for a few days without being build by hydra. That wasn't considered an issue because it was not 'stable'
<MichaelRaskin>
In the meantime, stable goes a few days without any updates.
<obadz>
MichaelRaskin: only if someone bothers to package the bugfix. In general people just cherry-pick from master..
<obadz>
Yeah exactly. That's not great from a security standpoint..
<MichaelRaskin>
To begin with, _upstream_ packaging a bugfix release in parallel to normal release increases the chances of success.
<MichaelRaskin>
I dunno, I am not a -stable user, and separately not a NixOS user (I have a good chance of giving up my last NixOS installation) — I am Nixpkgs user and my kernel is from Nixpkgs, but NixOS… I don't care that much.
<obadz>
oh? dare I ask why?
<obadz>
systemd?
<MichaelRaskin>
Where do I begin.
<obadz>
if you have nixpkgs kernel and apps, there's not much else you're giving up other than systemd
<MichaelRaskin>
But yes, the ugly in the mix are a few properties of systemd
<MichaelRaskin>
Oh, I also prefer that my interaction with NixOS modules system is blackbox function-like
<MichaelRaskin>
I am OK asking «give me the /etc/X11/xorg.conf of the system with that stripped-down configuration»
<MichaelRaskin>
I do not want to negotiate the mount system with NixOS modules for boot.
<MichaelRaskin>
I am not too happy about NixOS bootloader config generation, I don
<MichaelRaskin>
I don't like what it does with /etc/ switching too much…
<MichaelRaskin>
But yeah, if systemd was not spreading over everything, I would probably put up with that.
neuralring has quit [Quit: Leaving]
nrdevilspgd has joined #nixos-chat
nrdevilspgd has quit [Client Quit]
<MichaelRaskin>
obadz: but I feel like stable being just the most critical bumps from master and old everything else is actually what some people want.
<MichaelRaskin>
Even if it turns out that stable gets strictly a subset of master commits, this won't convince people who want exactly that…
<obadz>
what actual distro do you use?
<obadz>
arch?
<obadz>
have you considered clever's not-os
<MichaelRaskin>
I use Nixpkgs kernel, I am not sure any distro will let me do that without going crazy
<obadz>
I see so you use your own handrolled distro build using nix
<obadz>
pretty cool
<MichaelRaskin>
After A/B LFS — writing a script to mount my partitions is the easy part, it is the glibc build where I can benefit from the other people's work.
<MichaelRaskin>
And that mini-distro is slowly being more and more controlled by Common Lisp code starting from the middle glue layer.
<obadz>
you're rewriting systemd :')
<MichaelRaskin>
obadz: in my submission to ELS I actually point out a few differences.
<MichaelRaskin>
1. I write code in a way that it makes sense to define policy by loading code that adds — or overrides — some parts of the controlling daemon, not by fighting the constantly changing configuration system (see: logind & linger)
<MichaelRaskin>
2. I aim to be able to have multiple independent daemons with minimal (and well-defined) interaction that can arbitrarily divide obligations
<obadz>
have you presented this at a meetup?
<obadz>
(what's ELS?)
<obadz>
MichaelRaskin: in which geography are you?
<MichaelRaskin>
European Lisp Symposium
<MichaelRaskin>
Currently Bordeaux
<MichaelRaskin>
Not aware of any meetups nearby…
<obadz>
if you're ever in London, I'm sure zimbatm (and I) could set up a meetup for you to present this
<MichaelRaskin>
I guess after ELS — I hope the submission where I tried to focus on the Lisp part with Nix being just a tool to manage all the annoying non-Lisp stuff will get accepted — I might start writing something about the Nix part.
<zimbatm>
MichaelRaskin: yup, I would be happy to host a talk for you
neuralring has joined #nixos-chat
* sphalerite
would try and come down as well
<MichaelRaskin>
I wonder if one of the fractures in the Nixpkgs is pet-vs-cattle attitude difference with respect to packages…
<MichaelRaskin>
One side's dream is careful proactive maintenance. The other side's dream is automated bump, a few tests of reverse dependencies, auto-merge, and a revert if anything is reported wrong.
neuralring has quit [Quit: Leaving]
<shlevy>
obadz: I think the ofborg efforts will help with master being broken as often as it is.
<shlevy>
Personally I tend to end up back on master amonth or so after each relase historically, but for my clients/employers I prefer the stability of a release branch.
<sorear>
is this channel normally this ontopic?
<shlevy>
:D
<shlevy>
MichaelRaskin: +1 to pet vs cattle
<shlevy>
Despite the, um, friction involved there I actually think the hackage vs stackage distinction is something we could move toward
<MichaelRaskin>
sorear: have you missed all my ranting about how Thing X That Is Also Wrong is _also_ a victim of a bad Nash equilibrium?
<shlevy>
Curated package set on top of a "throw the latest of everything in there" free-for-all
<sorear>
MichaelRaskin: i joined a few hours ago to talk about real numbers in new foundations, since then it's been nix this nix that
<MichaelRaskin>
I, personally, think even the _curated_ set is cattle. Just with a better defined standard of care (some autotests, repology and upstream homepage cross-checks), but still cattle
<shlevy>
Anyone have any opinions on open hardware platforms?
<sorear>
term is insuffiently well-defined for a meaningful answer.
<shlevy>
Aww come on that was a perfect opening :P
<MichaelRaskin>
(I don't see any resources to scale our processes to allow collaboration of enough people to maintain carefully groomed packages at the level of 10% of the current number)
<MichaelRaskin>
sorear: wait, even after NF we talked about utility functions?
<shlevy>
MichaelRaskin: Agreed, ultimately. I think if we manage to make nixpkgs actually modular and figure out the IFD/recursive nix issue then people who want to maintain their own packages well can do so in isolated efforts.
<MichaelRaskin>
But yes, this channel is bursty, and obadz directed the one more burst to be about Nix
<MichaelRaskin>
shlevy: I guess people who are actually willing to maintain a small amount of packages well will eventually be given the access to do this directly in Nixpkgs. Admitting that the majority of packages is not like that is still needed.
<MichaelRaskin>
Then again, even for closely groomed packages some cattle-style (epizoothy-prevention?) edge conditions will still be enforced — in a cattle-like manner.
<MichaelRaskin>
Like, anything that breaks eval gets blocked or reverted, be it a bot, a push hook, or an annoyed ofborg user.
<MichaelRaskin>
Even if it improved the actual build in the process of breaking meta…