<clever>
infinisil: that is one of the entiries in the DB!!
<infinisil>
Yeah that's what I mean :P
<clever>
ah
<infinisil>
Sneaky bunch, these people who wrote it
<clever>
computers-Unix will self-destruct in five seconds... 4... 3... 2... 1...
<infinisil>
> lib.length fortunes
<{^_^}>
1361
<infinisil>
> fortune
<{^_^}>
"You're being followed. Cut out the hanky-panky for a few days."
<infinisil>
Only computer-related quotes now, or actual fortunes such as this ^^ are in it now
<samueldr>
what didn't make the cut?
<samueldr>
well, what kind
<infinisil>
samueldr: There's all kinds of categories, check out cd $(nix-build --no-out-link '<nixpkgs>' -A fortune)/share/games/fortunes
<infinisil>
I only used categories linux, linuxcookie, computers and fortunes
<samueldr>
uh, weird issue with my setup I hadn't thought about, buzzing noise when I don't plug in my iPod (3rd gen classic) (it's in the line-in of my computer)
* infinisil
is unsure if that's expected or not
<samueldr>
yeah, noise interference from the cable
<samueldr>
once plugged-in, the circuit is complete
<srk>
noise pickup is hell, I'm close to giving up on jacks and switching to TOSLINK
<srk>
or balanced cables at least
<samueldr>
heh, noise isn't much an issue with my setup since it anyways mostly get compressed in A2DP
<samueldr>
nsfa: not safe for audiophiles
<srk>
pretty much :D
<samueldr>
I do hear the noise from the botched upgrade to SD cards in the iPod
<samueldr>
when there's silence AND data transmission going on
<srk>
we've tried one of these bluetooth things at our hackerspace but promptly switched back to cables :D
<samueldr>
(there was no shielding at all stock, that's normal, and nothing prescribed from the board makers)
<srk>
with notebooks it's even worse - internal soundcard in my x230 is crazy noisy
<srk>
like you can identify hardware components by the noise ..
<samueldr>
haha yeah I know the feeling
<samueldr>
(hdmi sound output helps reducing the sources)
<srk>
I'm experimenting with few ADC/DAC chips and USB I2S on STM32F4
<srk>
want to write my own firmware for that when I figure it out :D
<srk>
mainly USB -> DMA -> I2S /o\
<clever>
srk: one of my projects in the past, was to make a 32 channel audio capture rig
<clever>
thats ~70mbit worth of bandwidth
<clever>
and USB latency is not up to the task
<srk>
yeah, I'm considering building 8 channel one
<clever>
my plan was to use an FPGA to directly stream it into ethernet
<srk>
not sure about USB either, like it's probably doable sa there are focusrite USB soundcards with 8+ channels
<samueldr>
why not just use a bunch of pis with cheap 2$ aliexpress usb card ;)
<samueldr>
don't enumerate the reasons! it's obviously satire
<srk>
fee weeks ago I've almost bought 10 channel PCI rack soundcard
<srk>
cost effective solution :D
<srk>
but it might be doable with ice40
<clever>
srk: my plan was to have rack-mounted boxes that can do either in or out, with modules for either
<clever>
and a max of 32 in either direction
<clever>
then ethernet to run the audio to a mixing station
<srk>
mm, cool :)
<clever>
and the mixing station would just be a server with drivers to expose the streams to the standard API's
<clever>
then normal mixing software takes the rest
<clever>
but i never finished that project
<srk>
with FPGAs it looks even easier as you don't need TCP/IP, just roll your own dumb bus with muxed i2s or something
<clever>
UDP is trivial to do with an fpga
<clever>
just shit packets out the port blindly
<clever>
the hard part, where i got stuck, was implementing DHCP in verilog
<srk>
hehe, got to try :)
<srk>
want to write something in clash
<clever>
and i also wanted avahi
<clever>
i wasnt into functional things then
<srk>
:D
<srk>
I wrote ZRE implementation for haskell that would be ideal for stuff like sensors, home automation things (instead of avahi) but it's even more complex due to zeroMQ
<srk>
I'm using avahi with nodeMCU on esp8266, work fine but sometimes I'm getting System error when I try to ping the devices from nixos, not sure what's going on
<clever>
srk: my solution to these problems, was to make the fpga act as an SPI based ethernet card
<clever>
then write a linux driver for it on the rpi
<srk>
(fedora doesn't have this issue)
<clever>
so on the surface, its just an rpi using an abnormal ethernet card
<srk>
heh, we wanted to do SD card emulation for SBCs
<clever>
but, via a side-channel, the rpi can then enable audio capture channels, and set target ip's
<srk>
as it's faster than 100mbit ethernet
<clever>
the "ethernet" card will then inject its own packets into the ethernet
<clever>
and the rpi wont even notice them
<srk>
:D
<clever>
so basicaly, the ethernet card will mitm its host, and start its own convos on the network
<clever>
forcing horror stories to work for me!
<srk>
we wanted to do something very similar but decided to do it with more powerful board - LS1046 64bit arm with ECC support
<srk>
plan is to try attaching ECP5 which would emulate storage, network and console over PCIe, hypertransport or our custom fabric (not decided yet)
<srk>
(or "less crippled board" :D)
<clever>
clash might allow large chunks to be done in the fpga
<srk>
for ethernet you can do what you mentioned - just shove packets to dumb endpoint and handle everything on the other side
<srk>
I wish thoughpolice fixes clash-playground soon :D
<clever>
the hard part, is configuring that endpoint, what channels to capture, and even discovering the fpga on the LAN
<srk>
I'm afraid I need to learn verification techniques to be able to write sane fgpa things
<clever>
i used iverilog and gtkwave for most debug
<clever>
iverilog lets you compile verilog to x86, and script dummy inputs and read files
<clever>
gtkwave lets you view the waveform recordings iverilog makes
<joepie91>
working on a modelling/typing/constraint/whatever thingem for JS
<joepie91>
and just realized that this will probably make it possible to do things like db.insert(whateverObject) and have it Just Work o_O
<joepie91>
(no, it's not static typing)
<samueldr>
» var a = { }; a.a = a; db.insert(a)
pie_ has joined #nixos-chat
pie__ has quit [Remote host closed the connection]
<samueldr>
(I'm not doubting this can be solved, and probably relatively easily)
<joepie91>
samueldr: what I'm implementing basically has something like traits in Rust, so types can specify an implementation for a particular trait that works for that type
<joepie91>
samueldr: so it'd be possible to just have something like a DatabaseInsertable trait that specifies the exact semantics for inserting that particular type into a database, and db.insert(...) could then just blindly call/access whatever properties are relevant to that purpose
<joepie91>
it's a bit difficult to explain the whole thing :P
<joepie91>
somewhat experimental project
<samueldr>
:)
<drakonis>
gchristensen, when did you leave tumblr?
<joepie91>
samueldr: the goal is basically to make modelling of complex state easier and more reliable (through best-effort runtime validation), without significantly impacting either performance or developer ergonomics (taking into account 'idiomatic' JS)
<joepie91>
so it's not exactly static typing, it's not exactly traits, it's not exactly a validator library; it's a little bit of everything
<samueldr>
a bit of nothing, a bit of everything
<samueldr>
don't out-nix nix in name
<joepie91>
hehe
<joepie91>
samueldr: on a related note, I recently learned that Perl 6 has value constraints natively
<joepie91>
so like...
<samueldr>
last I heard of perl 6 it was vaporware... but I definitely haven't heard much about it since... almost ever
<joepie91>
subset Pincode of Str where /^ \d\d\d\d $/;
<samueldr>
(the kind of vaporware where the vapor visible, but no one uses it?)
<joepie91>
my $adhoc where *.elems == 5;
<joepie91>
etc.
<joepie91>
(those are runtime checks)
<joepie91>
samueldr: apparently it's not totally vaporware
<samueldr>
interesting ergonomics
<samueldr>
as in really interesting
<joepie91>
samueldr: these are basically the ergonomics I'm implementing in my JS thing; by chance, somebody I know who works on Perl 6 recently mentioned that this is already a thing there
<joepie91>
similar to a scary degree
<joepie91>
especially since I've never even looked at Perl 6
<joepie91>
but yeah, these kind of value constraints are something that I've been missing in most every type system so far
<joepie91>
somehow most interpretations of 'type system' seem to stop at defining 'a type' as 'an internal data structure'
<joepie91>
rather than including the space of valid values as well
<joepie91>
(semantically valid)
<samueldr>
right!
<joepie91>
it's also a big part of why I'm extremely skeptical of static typing arguments :P
<samueldr>
static types can still be wrong :)
<samueldr>
like functional programming can still have bugs
<samueldr>
just functional bugs
<samueldr>
you can functionally program something to be wrong :D
<samueldr>
and it's even demonstrably and provably wrong :D
<joepie91>
samueldr: right, my issue with static typing systems that don't do value constraints is that you're paying 90% of the cost of type declarations but you only get a fraction of the possible benefits...
<joepie91>
add value constraints and suddenly you can prevent *so many more* types of errors
<samueldr>
I tend to agree, if it's impossible to fit the square peg in the round hole, while all of them are Hole, it's probably better in the end
<joepie91>
(most of the code there works, right now I'm working on the traits)
<joepie91>
(and .unique is not yet implemented either)
<samueldr>
oh, IRC
<joepie91>
yeah
tertle||eltret has joined #nixos-chat
<samueldr>
protocols, line-based, are a good match for this
<joepie91>
samueldr: originally started this in the context of an experimental IRCd project :D
<joepie91>
(user and channel persistence, multi-device support, etc.)
<joepie91>
so all this stuff is coming from my Lab Of Mad Software Science
<samueldr>
free idea: don't implement a custom server protocol, or even irc server protocol, for linking servers, use something like rabbitmq
<samueldr>
(if you ever expand on the idea)
<ekleog>
joepie91: you want dependent types, I think (for semantically valid types only)
<samueldr>
(irc server protocol as per the RFC I meant)
<ekleog>
issue is, dependent types require a full-blown theorem prover in the compiler, and often you have to give it hints
<ekleog>
F* is the least bad option currently, from what I heard
<joepie91>
ekleog: all validation here is runtime, so I can cheat on that a bit I think :)
<joepie91>
ekleog: and you can already implement this with the generic .validate modifier, I think
<ekleog>
yeah, if you implement validation at runtime you don't need any of this, but you have to handle typing errors at runtime :)
<joepie91>
yeah, that is the idea
<joepie91>
like, this isn't meant to replace static compile-type checks
<ekleog>
I meant when you say that you don't like static typing, it's just that you should be using dependent-typing static type systems (also sometimes called provers) :°
<joepie91>
it's meant to replace the hodgepodge of validation libraries, collection management, and ad-hoc guards that tend to be littered throughout JS projects
<joepie91>
ekleog: that's not what I said! :P
<ekleog>
hopefully someday research will make it easily usable :D
<joepie91>
it's static typing *arguments* I'm skeptical of
<joepie91>
99% of them are made by people who wouldn't know what dependent types are if their life depended on them
<ekleog>
indeed, I over-stated it a bit :)
<joepie91>
they just have some nebulous impression that annotating things with 'string', 'number', etc. will magically fix their code
<joepie91>
and I'm only exaggerating slightly
<ekleog>
(though I personally think the type system catches at least quite a few errors [at least if I can believe the number of errors rustc spits at me everytime], like rust's lifetime handler encoded in the type system that makes it easy to have safe non-GC'd values :))
<joepie91>
ekleog: it's extremely dependent on code style, in my experience
<ekleog>
one of the best arguments for static typing (to me) is that when you refactor, you usually just have to follow compilation errors and in the end It Just Works(tm) (though not all the time)
<joepie91>
there's a large overlap between 'errors that static typing catches' and 'errors that are prevented through loosely coupled abstraction', though the latter set is much bigger
<joepie91>
ekleog: I actually really dislike that approach
<joepie91>
it tends to cut out a necessary mental step of considering whether things *make sense*
<joepie91>
resulting in code that's refactored to make optimal sense to a computer, but not necessarily to a human
<joepie91>
such hints can be useful during refactoring, for sure, but they probably should not *lead* your refactoring process
<joepie91>
anyhow, I find that static type validation catches many errors in what would otherwise be tightly coupled spaghetti, but that it turns up almost nothing in well-abstracted code
<ekleog>
well, I mean, typically my last big refactoring was changing a string type from an either borrowed-from-exterior or self-owned type to a always-refcounted type, and I was very happy to know I could not have missed one occurence where a method would have to change name :°
<joepie91>
both from personal and third-party experience :p
<joepie91>
ekleog: right, refactoring that doesn't involve structural changes probably doesn't need that 'does it still make sense' step as much; but it's also not something I'd typically call 'refactoring', it's a fairly small change
<ekleog>
and the thing is the “almost” in “almost nothing”, to me :) (then, the fact it's possible not to have a GC, too, but that's only rust, not really all static typings)
<ekleog>
well, even with the compiler it took me a full week-end ^^
<ekleog>
(had quite a mess of lifetimes to change around everywhere)
<joepie91>
there's a cost to static typing :P so 'catches a few issues' does not necessarily justify its use, depending on case
<joepie91>
(developer cost, that is)
<ekleog>
hmmm I personally develop faster with static typing, mostly because I'm forced to first think of the API instead of rushing to the code, but I guess that's developer-dependent :)
<ekleog>
(also, I've seen way too many TypeError in people doing python's code to really want to go back there, even though I haven't personally hit that many)
<joepie91>
ekleog: this is also very much down to how you approach development, and how much experience you have in eg. working with abstractions
<joepie91>
ekleog: like, one big problem that JS has for example is that its insane flexibility in abstractions makes it very easy to write very reliable code *once you understand how to do abstractions*, but until that point it seems like an unpredictable and volatile language that just produces bugs
<joepie91>
so if you've never invested particularly much effort into writing reliable JS, yes, you will develop faster in something that's much stricter about eg. types
<joepie91>
but if you *have* invested serious effort into writing reliable code through abstraction, suddenly stricter languages can't compete in that area anymore
<ekleog>
one big problem with JS is that the language is actively trying to get you in its traps, just like C or C++ (and I say this while I'm still a C++ fan, so it's not meant as an insult :p)
<joepie91>
but this is not apparent at the outset
<joepie91>
ekleog: JS has relatlvely few traps (that I'd nevertheless like to see disappear)
<joepie91>
mostly stuff like == vs. ===
<joepie91>
and implicit type conversion
<ekleog>
exactly these
<ekleog>
(also, performance traps, but I see them mostly because I've worked much longer on a JS JIT than with JS itself, I guess)
<joepie91>
if there were a flag to disallow those two, I'd use it :P
<samueldr>
I see how static types make better ABIs
<joepie91>
ekleog: anyhow... you referred to 'first think of the API instead of rushing to the code' - once you grok how to work with abstraction, you end up doing the same
<ekleog>
like, “hey frozen objects are actually slower almost everywhere”
<joepie91>
so that benefit is not obtained exclusively from static typing :D
<joepie91>
ekleog: what's the cause of that anyway?
<ekleog>
well, the difference is that then you have to consciously take this step every time :) I mean, if you, in your mind, do the work of the typer, then you can do the same with dynamic typing as with static typing, but it's just additional brain usage (to me)
<joepie91>
ekleog: no, it becomes an automatic habit
<ekleog>
samueldr: Also, it allows more easily to make sure one's APIs don't change over time due to a seemingly-unrelated thing :)
<joepie91>
and it's not so much 'do the work of the typer' as it is thinking about what data you have and how it relates to other data
<joepie91>
that goes beyond what static typing typically introduces :P
<ekleog>
<joepie91> ekleog: no, it becomes an automatic habit <- well, remembering to free() stuff was also an automatic habit when I did C, it didn't prevent me from sometimes forgetting and losing unconscious brain power :)
<joepie91>
ekleog: that is not quite the same; free()ing is something contextual that requires conscious consideration to get it right, whereas 'start out with a data model' is something that applies in 100% of cases and isn't really contextual
<ekleog>
(otherwise, I personally have types enforce their own invariants, so each can actually only contain what it's supposed to contain, and I create a new type if I've got a new type of invariants, so static typing does do a lot already)
<ekleog>
<joepie91> ekleog: what's the cause of that anyway? <-- you must throw an exception if trying to change a property, compared to just doing nothing, that's an additional check and bailout reason (especially violent against frozen arrays)
<ekleog>
anyway, gotta go, sorry :)
<joepie91>
haha, np, good conversation :)
drakonis has quit [Remote host closed the connection]
drakonis has joined #nixos-chat
sir_guy_carleton has quit [Quit: WeeChat 2.0]
drakonis has quit [Remote host closed the connection]
Guanin has quit [Ping timeout: 248 seconds]
Guanin has joined #nixos-chat
pie_ has quit [Ping timeout: 248 seconds]
tertle||eltret has quit [Quit: Connection closed for inactivity]
<joepie91>
ValidationError: Expected object of a type with the OnlineIdentity trait, got BullshitIdentity instead
<joepie91>
progress :D
<etu>
Haha
__Sander__ has joined #nixos-chat
<ekleog>
[insert here a troll about dynamic vs static type systems 😇]
<gchristensen>
Drakonis[m]: february
<andi->
Just finished migrating an internal service to a nix expression (including a docker image & VM tests).. Initial feedback from colleagues: The syntax is weird... Guess they don't see the immediate value of being able to declare how the test infra should look like etc... They like the customized docker images tho... :~:
{^_^} has quit [Remote host closed the connection]
<sphalerite>
andi-: "customised" how?
<andi->
sphalerite: well just containing that one binary that I built from the rust project (and it's dependencies) compared to the pain of doing that with multistage builds or pacakging an entire debian in there...
<sphalerite>
aaah right
<sphalerite>
well sounds like a good start!
<andi->
yeah.. It's a tough one to convince the Debian People that theres a "better" way :)
<sphalerite>
I was convinced before I discovered nix, just didn't know the better way had been implemented yet :')
<LnL>
just went from nothing to running our entire testsuite with nix on somebody's machine under 30s :D
<gchristensen>
nice!!
<sphalerite>
LnL: \o/
<sphalerite>
this calls for ice cream! :p
<LnL>
TIL nix complains if /homeless-shelter exists
<gchristensen>
:o
{^_^} has joined #nixos-chat
{^_^} has joined #nixos-chat
{^_^} has quit [Changing host]
Sonarpulse has joined #nixos-chat
sir_guy_carleton has joined #nixos-chat
<gchristensen>
anyone want to be my robot army and upvote my thing here: https://lobste.rs/
<andi->
great excuse to finally create an account...
<gchristensen>
I can invite you if you need
<andi->
argh, it was invite only..
<andi->
sure go ahead
<gchristensen>
emil?
<gchristensen>
email*
<andi->
have to create one for that... 1 minute
<gchristensen>
:o
* andi-
unpacks private notebook to create a new subdomain
<gchristensen>
man
<andi->
gchristensen: you got a PM
<gchristensen>
I'm surprised you didn't register a new ASN for this
<gchristensen>
invited
<andi->
lol
<andi->
I'd be broke if I had an ASN + IPspace for every mailinglist/account
__Sander__ has quit [Quit: Konversation terminated!]
<maurer>
Homotopy type theory is cool, did you discover an application for it?
<maurer>
Even the people I know doing PhDs in it don't have any idea of something it'd be useful for
<drakonis>
no, sadly not
<drakonis>
someone else did tell me an application
<drakonis>
it can be used for building superpowered nix
<maurer>
You can't even extract from the proof to a running code due to no interpretation for rewriting a type via a path
<maurer>
In what sense?
<drakonis>
apparently automatically traveling through repository forks and handling merge conflicts
<drakonis>
its complicated
<maurer>
I am suspicious that this is either attributing powers to HoTT that it doesn't have, or of using a sledgehammer to drive in a nail
<maurer>
but I can't really evaluate without more details
<drakonis>
this is what i was told "basically what it would let you do is move from a repository you have, which may be a fork, to another fork automatically even though they may have different histories from some baseline because there exists a path in a topological space of that repository between them and you could statically check whether or not you can apply that change i.e. you don't ever run into merge conflicts that screw up your repo it will
<drakonis>
tell you ahead of time what the problem is"