<elvishjerricco>
clever: I think reserved space could do it though, right?
<clever>
nix is supposed to delete that before doing operations, to give itself enough room
<elvishjerricco>
Make it impossible to create the snapshot that makes it impossible to delete a file
jasongrossman has joined #nixos-chat
<elvishjerricco>
Ah ha!
<elvishjerricco>
Create a ZFS pool. Fill it completely with a file. Open that file with `O_WRONLY | O_SYNC`. Write different data to it.`No space left on device`, no snapshots needed
<elvishjerricco>
Er, ok O_SYNC isn't necessary. I thought that's what made the difference. Hm...
<elvishjerricco>
Nope, apparently it's some difference between open and fopen
<gchristensen>
isn't this why zfs lets you reserve space?
<elvishjerricco>
gchristensen: I'm mostly trying to find the limits. i.e. how does ZFS allow me to overwrite this file at all if it has no space for CoW?
<elvishjerricco>
it seems it *doesn't* allow me with open, but does with `fileno(fopen(...))` for some reason.
<gchristensen>
you might find #zfsonlinux an interesting place :)
<elvishjerricco>
I wish :P They ban irccloud outright
<gchristensen>
right
<elvishjerricco>
Ah, it's O_TRUNC
<elvishjerricco>
So ZFS is able to truncate a file with no space remaining
<elvishjerricco>
clever: So you could have solved your problem with `trucate -s 0 /nix/var/nix/db/reserved`
<gchristensen>
elvishjerricco: want a NixOS user cloak?
<clever>
elvishjerricco: in the past, i have solved my issue with `echo -n > something`
<clever>
> opens with truncation, `echo -n` writes nothing
<{^_^}>
error: syntax error, unexpected WITH, expecting ')', at (string):243:7
<gchristensen>
ooh what happens if you truncate the file another process has it open
<elvishjerricco>
That's a scary thought :P
drakonis has joined #nixos-chat
<gchristensen>
because I expect it'll keep the space until the other handles close, which is what other filesystemts do
<clever>
gchristensen: i believe the reads will start returning eof, because the read pointer is now beyond the eof
<elvishjerricco>
clever: I'm not sure why that would work though. If there exists a snapshot of `something` already, that should fail
<gchristensen>
well, think log files -- all writes
<clever>
elvishjerricco: dont remember the exact condition where that worked
<clever>
gchristensen: ive seen tail mess up, when a log file gets truncated and its reading at the wrong offset
<elvishjerricco>
Wonder if new logs would leave a sparse hole in the file or continue at the beginning
<gchristensen>
a classic newbie mistake: disk full -> delete a bunch of log files -> data not reclaimed -> HELP (answer: restart the daemons to get them to reopen their logs)
jasongrossman has quit [Ping timeout: 255 seconds]
<clever>
gchristensen: years ago, ive reclaimed 10+gig of space, by just restarting daemons
<gchristensen>
bingo
jasongrossman has joined #nixos-chat
<Ralith>
yet another reason to just call out to journald
<Ralith>
logging: more gotchas than you'd think!
<clever>
Ralith: i think journald handles the above problem better then syslog-ng
<clever>
pretty sure syslog-ng forces a sync after every single line
<Ralith>
that sounds pretty terrible!
<Ralith>
journald handles a lot of things nicely
<Ralith>
it is a nice tool
<elvishjerricco>
Looks like I was right. ZFS is not atomic at the syscall level. I just did an experiment with cutting power during a big `write` with `O_SYNC`, and unsurprisingly got a partial write.
ninjin has quit [Ping timeout: 256 seconds]
ninjin has joined #nixos-chat
<ldlework>
drakonis: yo! wanna play?
<drakonis>
ldlework: its kinda late tho
<drakonis>
1:30a,
<ldlework>
oh yeah just noticed
<drakonis>
am
<ldlework>
drakonis: ping me when you wanna
<drakonis>
gotta get up early
<drakonis>
did i get the right account tho?
<ldlework>
yeah
<drakonis>
really gotta change the id
<drakonis>
seems kinda weird
<ldlework>
ldlework?
<drakonis>
no
<drakonis>
the vanity id
<ldlework>
Muslim Zionist?
<drakonis>
yes
<ldlework>
why?
<drakonis>
seems kinda weird vOv
<ldlework>
do you know what it means?
<drakonis>
yes
<ldlework>
what's weird about it
<ldlework>
other than the obvious
<drakonis>
just the obvious
<ldlework>
(it's largely an oxymoron)
<drakonis>
yes
<ldlework>
so people shouldn't use oxymorons as their vanity id and should change it?
<elvishjerricco>
George Michael in Arrested Development season 5 really had a simple solution to his problem: Tell the team he got by accident to start working on v2. That's like software startup 101. v1 is crap, v2 is just as crap but you spent more money on it so it's worth more.
<Taneb>
ldlework: what's Risk of Rain 2? Other than today's weather report
<andi->
Taneb: an awesome game :)
<andi->
elvishjerricco: that reminds me of the bullsh^Wlogic I am confronted with at the company... Whatever time we spent "generates value".. Not entirely sure how they think that can possibly always be the case for any kind of activity but thats not my problem.
<andi->
replacing a broken SSD likely ensures future value but doesn't really create any..
<Taneb>
I can understand that logic, to some extent
<andi->
to some extend yes
<Taneb>
Ensuring future value is definitely valuable
<Taneb>
Just not all (or even any, sometimes) of the value ends up in the product de jour
<andi->
e.g. refactoring code must be sold as a user story that improves value even thought it probably just reduces future development time and aids the value creation.. (realisticly it is just a value transfer, they pay sallaries and get "value" for it; i hate the "generated" aspect of it)
<andi->
and the value is also estimated by the developers...
* andi-
shakes head and mumbles on
<jasongrossman>
andi-: That sounds frustrating to me.
<andi->
It is.. on the other hand I create value all day long! I must be a huge value-generation-asset!!!
ma27 has quit [Quit: WeeChat 2.4]
ma27 has joined #nixos-chat
ma27 has quit [Ping timeout: 245 seconds]
ma27 has joined #nixos-chat
ma27 has quit [Quit: WeeChat 2.4]
<eyJhb>
It is a weird feeling, when you feel like your are doing the most hacky, janky, `just works` solution, and a mod says "It is the best way to do it for your requirements".
<eyJhb>
And I slowly feel like I am killing the projekt I am working on
ma27 has joined #nixos-chat
Myhlamaeus has quit [Ping timeout: 264 seconds]
<andi->
so DO Spaces with their "CDN" also has a lot of 504 for my bucket... Something about S3 seems to be very hard for CDNs..
<andi->
or maybe nix requests too many 404s...
ninjin has quit [Quit: reboot]
drakonis has joined #nixos-chat
waleee has joined #nixos-chat
jasongrossman has quit [Ping timeout: 255 seconds]
jasongrossman has joined #nixos-chat
drakonis_ has joined #nixos-chat
drakonis has quit [Ping timeout: 252 seconds]
jasongrossman has quit [Ping timeout: 240 seconds]
drakonis has joined #nixos-chat
joepie91 is now known as joepie912
joepie912 is now known as joepie91
<Taneb>
Random thought: torrenting nix outputs
<gchristensen>
yeah, it has been explored. however, the time to establish peers is very slow, and this is compounded 1 zillion times -- once per derivation built, to see if it is cached or not
<__monty__>
gchristensen: Why not have the daemon always in a DHT?
<Taneb>
:)
<gchristensen>
that is certainly something you could explore, __monty__
<Taneb>
gchristensen: it's reassuring when someone else has already explored my random thoughts
<gchristensen>
one way to explore this without writing it right in to nix's daemon is to build an http <-> DHT proxy thing in whatever your favorite language is
<lassulus>
twitch livestreams of nix-build processes so people can fire them up and pretend to be working on something
<__monty__>
gchristensen: Yeah, that's a great idea. It's going on the list : )
<gchristensen>
oh man I would be so expert at that, lassulus :D
<infinisil>
"The more experienced a respondent is, the more likely they are to say blockchain technology is an irresponsible use of resources."
<joepie91>
pfffhrt
<joepie91>
not a surprise
<clever>
infinisil: proof of stake!
<__monty__>
Kinda sad numbers for foss. 60% of people (on SO) contribute <1/year.
<__monty__>
Lol, 70% of people on SO think they're above average...
<clever>
thats not how averages work, but the sampling may be skewed
<clever>
total idiots arent going to go onto stackoverflow :P
<Taneb>
I don't think it's unreasonable that the average stackoverflow user is more competent than the average developer at all
<__monty__>
So biased towards Elon too...
<__monty__>
Taneb: I'd need convincing of that.
<Taneb>
__monty__: being willing to ask for help is a good attribute to have for a developer
<__monty__>
Most of SO's users don't post questions.
drakonis has quit [Quit: WeeChat 2.3]
<infinisil>
But also, there's probably some overconfidence in there
<__monty__>
They just search and copy/paste.
<clever>
i once had an android problem, found a question with the same problem, unanswered
<Taneb>
And browsing a website full of questions and answers isn't the worst way to learn new things
<__monty__>
Wow, vim so much more loved than emacs o.O
<clever>
so i just solved the issue myself, and recorded the fix there :P
<clever>
that answer now accounts for 90% of my upvotes on stack overflow
<infinisil>
clever: Yeah like 20% of posts get 80% of updoots
<infinisil>
I also have a couple Q/As with a whole bunch of votes
<infinisil>
But many with very little
<Taneb>
The "sexuality" question doesn't have an option I'd be comfortable calling myself (I'm asexual)
<samueldr>
sorry, you apparently are anexistant
<samueldr>
(according to a limited survey)
<Taneb>
It's a frustratingly common occurence
<samueldr>
any identity question through a selection is like having a select box for your name; you aren't one of Alex, Bob, Carol, Dolores... then you don't have a name, sorry
drakonis has joined #nixos-chat
<__monty__>
No mention of haskell or nix, this survey gets a thumbs down from me: 👎
<Taneb>
samueldr: even an "other" option would do
drakonis_ has quit [Ping timeout: 250 seconds]
drakonis has quit [Ping timeout: 252 seconds]
<infinisil>
Taneb: I wish they would use gender-independent sexuality options, something like "attracted to <multiple checkboxes of genders>"
<infinisil>
Because straight means different things depending on what you are yourself, and what about non-binary people, what is straight then?
Myhlamaeus has joined #nixos-chat
<jD91mZM2>
Lmao I just forgot about --install-bootloader and was super confused as to why nothing happened
thePirateKing has joined #nixos-chat
<eyJhb>
__monty__: mostly becase you don't need a external pedal for vim
<eyJhb>
Didn't notice I was hours late for that one
<__monty__>
That's very brief in irc reckoning.
<eyJhb>
Yeah, I just forget to scroll down somtimes when I peak at the chat
<eyJhb>
__monty__: did you use a custom keyboard?
<__monty__>
I don't, no. I'm an adherent of the Beast.
<infinisil>
manveru: I don't like python either, neither for packaging nor for programming
<manveru>
eyJhb: for myself
<eyJhb>
Reminds me.... Matplotlib should be marked as broken for Python 2.7 on NixOS Stable
<infinisil>
Just a couple days ago I typed `quailty` instead of `quality` and it took me 10 minutes to figure out why my program wasn't working
<infinisil>
Python doesn't complain if you do that..
<manveru>
infinisil: luckily my company doesn't even consider it... OTOH we're using ruby still heavily and still have some perl from 2005 in production :P
<thePirateKing>
if you use vim, theres a plugin called python-mode which checks those things for you
<__monty__>
Word on the street is ruby's worse.
<infinisil>
I just found out about http://www.mypy-lang.org/ recently, a static type checker for python
<infinisil>
If I'd have to use python more often I'd give it a go
<thePirateKing>
ah yeah i have to use python every day and its a lifesaver
<eyJhb>
infinisil: I remember I did something even more stupid today... Switcher around a `lower, upper := funcCall()`, so it was `upper, lower := funcCall()`, spend a good 15 minutes debugging that shit..
<__monty__>
Requires annotations though, no?
<__monty__>
Can't really contribute that to random python projects.
<manveru>
__monty__: yeah, the only saving grace is that at least in ruby everyone uses the same way to package things :)
<infinisil>
eyJhb: Well admittedly I don't know of any programming languages that would prevent that
<eyJhb>
In Golang we even all format in the same way ;)
<eyJhb>
No, but that is just my pure stupidity. But I have done that multiple times in Python too!
<infinisil>
Oh right that's not python
<infinisil>
Wait go really uses := for assignment
<eyJhb>
infinisil: only to declare new variables, `var myString string` is valid as well
<manveru>
yeah, it's a shorthand for `var x int; x = foo()`
<eyJhb>
^^
<manveru>
s/int/whatever/
<eyJhb>
The good ol' `var x T` as used in most docs
<infinisil>
Huh alright
<infinisil>
Weird flex but alright
<manveru>
heh
<eyJhb>
But infinisil look up go format, it is awesome :p Enjoy having my if statements formatet for me
<thePirateKing>
go format is amazing
<gchristensen>
+1
<infinisil>
I sure do like autoformatters, wish I'd use a language that had one
<eyJhb>
Yeah, it is the saviour of my days.. COmbined with vim-go.. Format on each save.
<eyJhb>
*pst come join us
<infinisil>
Wait I use haskell which has an autoformatter, it's nice
<__monty__>
Dhall has it.
<manveru>
lots of languages do nowadays
<eyJhb>
I have never coded in haskell, but for some reason I cringe everytime I hear it. No clue why
<__monty__>
I'd expect rust to.
<gchristensen>
`cargo fmt`++
<__monty__>
eyJhb: Lot's of gophers do.
<andi->
we just need one for nix ;-)
<infinisil>
eyJhb: I love it! It's my go-to language for everything even mildly complicated
<eyJhb>
But they Might have a better reason to do so!
<__monty__>
Was on the indirect receiving end of some derision at a Go meetup.
<infinisil>
thePirateKing: Definitely, even if you're not going to use it, it teaches you lots
<eyJhb>
Mine were PHP for a long run, then Python and now somewhat Python. I still do enjoy Python for anything hacking related
<manveru>
infinisil: i just spent a week learning haskell :)
<thePirateKing>
yeah i want to get more into FP
<infinisil>
manveru: Nice
<manveru>
still haven't gotten auto-format to work right because of missing ghc-mod
<eyJhb>
Can ANY of you remember the anti-theft techs that were used in audio of e.g. cinema movies?
<infinisil>
manveru: I use stylish-haskell
<eyJhb>
So they weren't able to play them back on different entertainment systems that implemented it?
<samueldr>
no, but maybe a good starting point is a similar tech, macrovision?
<__monty__>
manveru: stylish-haskell, hindent or brittany are the options.
<tilpner>
joepie91: Yay, always good to see these :)
<__monty__>
ghc-mod is discontinued.
<manveru>
yeah... spacemacs haskell layer seems a bit outdated
<eyJhb>
samueldr: yeah, something like that. I just remember they encoded a datastream in the video/audio layers...
<infinisil>
__monty__: Well, it's still continued, but as a library exclusively
<__monty__>
manveru: Not necessarily, I think intero still uses ghc-mod.
<infinisil>
__monty__: I think at least
<__monty__>
It gets way less attention though.
<manveru>
__monty__: i switched to hie with lsp
<__monty__>
Not sure it's even meant as a library past intero anymore : )
<__monty__>
Ah, that uses ghc-mod as well?
<manveru>
but the autoformatting sometimes just... doesn't do anything
<__monty__>
I don't bother.
<infinisil>
manveru: I'm used hie with emacs, but the emacs client has some problems that make it a pain to use. The changes get out of sync over time, so I need to constantly restart it
<infinisil>
:(
<manveru>
jup
<eyJhb>
Are there any emacs users in here, which DO NOT use Evil Mode?
<infinisil>
manveru: Also with vim?
<manveru>
i didn't try vim
<gchristensen>
I don't, eyJhb
<__monty__>
I use hlint and ghcid.
<infinisil>
eyJhb: (not me, I use evil)
<__monty__>
None of the fancy options work very well.
<eyJhb>
infinisil: is.. Is sthat the same?
<eyJhb>
isn't that the same**?
<eyJhb>
gchristensen: and no emacs pinky or foot pedal?
<infinisil>
(I use emacs with evil mode, so I'm not one of the people you were looking for, not sure where the confusion is)
<gchristensen>
heh, eyJhb
<manveru>
eyJhb: he has a very special keyboard :)
<eyJhb>
Which keyboard do you use?
<gchristensen>
on a call
<infinisil>
manveru: Do you just live with restarting hie all the time?
<infinisil>
manveru: Or do you have something fancy against that
<eyJhb>
infinisil: ohh sorry.. :p Me that fucked up
<eyJhb>
gchristensen: "on a call"?
<gchristensen>
literally on the phone
<andi->
I tried using emacs without evil on regular keyboards but that basically amplified pain in joints/fingers/… with the kinesis it is bearable.. now I just feel crippled due to lack of knowledge compared to evil/vim mode
<manveru>
infinisil: no, i only learned it for a week, i'm back to elixir for now
<infinisil>
Ahh
<eyJhb>
Ahhh.... I will be waiting for my keyboard related answers then ;)
<manveru>
eyJhb: i think it was a kinesis
<gchristensen>
eyJhb: I use a kinesis advantage in multiple orientations and use my voice to code and dictate texts when I can
<eyJhb>
gchristensen: RSI?
<gchristensen>
I have fairly severe hand problems. emacs pinky isn't even on my radar :P
<eyJhb>
I know that feeling, except the rest of my body sucks too! :p Rocking my ERgodox-ez.
<manveru>
infinisil: not that i dislike haskell, but it just takes a lot of effort for me to be productive in it :|
<gchristensen>
heh
<eyJhb>
How well does voice dictation go?
<gchristensen>
it is challenging. learning dvorak / colemak / etc. vs. learning dictation-to-code is wildly different
<infinisil>
manveru: Yeah, sure does. It took me like 1-2 years of learning Haskell (admittedly very occasional) to first do something useful with it
<manveru>
infinisil: also, i learned via LYaH, which i heard was less than ideal
<__monty__>
gchristensen: Would be cool to see your workflow with dictation for 10-15min or something.
<eyJhb>
I wish I werent a Dane when it comes to dvorak/colemak. Would make it easier, as I wouldn't need æøå... - I could imagine dictation-to-code is hard
<infinisil>
manveru: I think it gives a great introduction, sure it has some problems, but the style in which it's written in compensates for that
<gchristensen>
manveru: I heard from a few people there were different "one true ways" to learn haskell, and I gave up because nobody agreed what it was.
<eyJhb>
__monty__ imagine gchristensen just code sprinting speaking 100+ works a minute
<eyJhb>
words**
<gchristensen>
manveru: imo, screw it, write some code
<eyJhb>
Wonder what it would be like sharing office with gchristensen
<gchristensen>
noisy :( luckily I work from home
<__monty__>
There's definitely not one true way. Current people's favorite in #haskell is CIS-194 (the fall course).
<manveru>
do you guys like idris?
<infinisil>
Although I think I mostly learned Haskell just by coding in it, just giving myself a goal and trying until I got it
<gchristensen>
^
<infinisil>
manveru: Love it!
<__monty__>
Yep, best way to learn any language really, just using it.
<eyJhb>
Trying to say that to people at my study.. But they don't know "what to code".
<infinisil>
(Although a tutorial at the beginning can't hurt, you won't know where to start without one)
<manveru>
__monty__: that was literally my first attempt a year ago :) wrote a savegame parser in haskell
<manveru>
but i didn't understand wtf i was doing, just brute-forcing different type signatures and stuff
<infinisil>
eyJhb: There's so many cool things to code, I can't believe so many people struggle with ideas
<manveru>
and the stdlib docs were very terse
<eyJhb>
infinisil: can you give me some that I can force feed them
<eyJhb>
Because currently the first project they are going to code is a simple neural network and make some feature extraction using OpenCV
<gchristensen>
they have to want it...
<eyJhb>
*force is the best way
<__monty__>
infinisil: I think the main problem is people want something interesting/fun/revelationy *but* not a lot of *work*.
<eyJhb>
But true ;) I just told them today, that I will not code a single line this semester
<infinisil>
Ideas for someone starting to program or?
<eyJhb>
After I ahve coded two workshops... - Yes
<manveru>
irc bots :D
<infinisil>
Hehe yes ^
<infinisil>
Or a simple programming language is very versatile
waleee has quit [Quit: WeeChat 2.4]
<andi->
that was my original thing when I learned C... Trying socket programming, protocol parsing, …
<infinisil>
Or a simple terminal game, online maybe, with a server for matching
<thePirateKing>
For me learning to hack with python was what got me into learning to code
<eyJhb>
infinisil: I think they will break there neck doing so. But it is a good idea!
<thePirateKing>
like a simple port scanner etc
<eyJhb>
I will pass it on :p
<eyJhb>
infinisil: a simple programming language?
<eyJhb>
manveru: IRC Bots.. Yeah that is always a good one! I remember my first one
<andi->
writing runtime "patches" for games cna also teach a lot.. Was great fun and learned a lot about computers, OSs, OpenGL, …
<infinisil>
eyJhb: What about a simple programming language?
<manveru>
eyJhb: my first one was in php :P
<eyJhb>
What do you mean with that? Making their own?
<eyJhb>
manveru haha :p It hurts to say, but I have some love for PHP deep down
<manveru>
php 2 or something...
<gchristensen>
manveru: jikes :)
<infinisil>
eyJhb: Yeah, write a parser, an ast checker, a code generator. There's a lot of interesting parts there
<infinisil>
Maybe brainfuck for a start would be fun
<manveru>
built it with a markov chain for answers, eventually took like a minute for it to answer because it had a huge unoptimized "db"
<eyJhb>
infinisil: we currently have about compilers at our university. I think they died a little inside because our lecture didn't really make it interesting at all...
<eyJhb>
But good point, it gives a good insight into programming languages
<manveru>
but hey, php got me into ruby, which brought me into smalltalk and lisp, and from there i learned so many languages i can't even list them all anymore :)
<infinisil>
eyJhb: What I like about compilers is that it's essentially just a pure function without sideeffects that takes an input string and outputs a string
<eyJhb>
manveru: and lets not forget, PHP is our friend online! All that insecure code!
<infinisil>
But there's so much magic behind a compiler
<eyJhb>
That sounds like a lot of my code basically
<manveru>
eyJhb: my local bookstore had like 3 programming books: C, Java, and PHP, i just chose the one that had the fastest results :P
<eyJhb>
But you're right, I will try to pitch a couple of things. But currently we are still at some hello world basics.. e.g. implementing counting sort would be a challenge for some...
<infinisil>
eyJhb: Oh something interesting I implemented when I started coding was simple encryption
<infinisil>
eyJhb: Like, just a program to input a text, a password and it will output the encrypted string
<thePirateKing>
caesar cipher is a fun easy coding project
<thePirateKing>
and caesar cipher breaker
<eyJhb>
I am close to just copy pasting this IRC Log and giving it to them :D Loads of great ideas!
<infinisil>
Yeah, or the slightly more complicated vigenere cipher
<infinisil>
Or how about an stdin/stdout calculator, a la `bc`
<thePirateKing>
that would be really informative
<infinisil>
stack-based (reverse polish notation) to make it simpler
<__monty__>
ASCII grapher.
<__monty__>
Z-machine interpreter.
<manveru>
pong :)
<eyJhb>
I have to sign out now ;) Thanks for the ideas! I will make a list of them tomorrow :D
<infinisil>
See ya :)
<thePirateKing>
later!
<manveru>
infinisil: so... do you know a bit more about the status of idris?
<manveru>
i saw it had a stable release, but they still say it's super experimental?
<infinisil>
manveru: It is usable and pretty stable, it won't change much
<infinisil>
But the author is working on a second version of idris, named Blodwen for now, which will be like idris, but much better, and written in idris itself
pie__ has quit [Remote host closed the connection]
<manveru>
oh sweet, chicken-scheme backend
<__monty__>
It's gonna be faster because it's implemented in a slower language? o.O
<infinisil>
(well not duh, because GHC (which idris1 is written in) is probably much more optimized than idris1 (which blodwen is written in))
<infinisil>
I think the algorithms and such is faster, asymptotically, or so
<infinisil>
Oh and it has much better support for linear typing
<infinisil>
Which I'm most excited about
<manveru>
i guess there's no way you can explain linear typing to me in a sentence or two? :)
<thePirateKing>
+1
<manveru>
well, or what it's good for
<infinisil>
Ah sure
<infinisil>
It allows you to annotate your function arguments with e.g. "1-use"
<infinisil>
This makes the compiler enforce that you can only use that argument once, and once only
<infinisil>
This means you can't write `dup :: a -> (a, a)` if the input is annotated like this
<infinisil>
Because you can't get a second a out of the input
<infinisil>
What this is useful for is two things (on the top of my head):
<infinisil>
- Allowing you to ensure that your program runs in *constant* memory
<manveru>
hmm
<gchristensen>
it is also neat because it can help promise you use all your arguments instead of mistakenly using one of them twice
<manveru>
"Linear types can be used to keep track of memory ownership, potentially to support region-based memory allocation, which promises memory safety without the overhead of tracing garbage collection."
<infinisil>
- Ensuring correctness. E.g. you shouldn't be able to just copy some resources
<manveru>
is that what rust does?
<gchristensen>
sorta!
<infinisil>
manveru: Yeah it's pretty much what rust does, minus mutability
<manveru>
ah cool :)
<infinisil>
Ah and yeah, no GC of course
<gchristensen>
I think Rust is an Affine type system
<infinisil>
It's the only way I know of to have a high level functional language without GC
<gchristensen>
with linear types you _must_ use each argument once, Rust can ignore args
<manveru>
don't you have to tell it to ignore it via the _ prefix?
<manveru>
pretty sure his compiler is smarter than me by now...
<infinisil>
Hehe
<gchristensen>
what is the difference between doing it in the type than doing it in code
<infinisil>
gchristensen: It's something inherent to the type, like rust's mut and & annotation things
<gchristensen>
I mean in themore general sense of Idris doing code-gen based on the type
<manveru>
it has functions _in_ the type definitions...
<manveru>
wtf is this
<infinisil>
gchristensen: Ah you mean that the compiler should be able to infer these annotations from the code?
<infinisil>
manveru: The magic of dependent types :D
<infinisil>
gchristensen: Oh wait, or not, I don't get you sorry
<gchristensen>
I guess I'm not sold that putting lots of thought-stuff in to types is any better than putting thought-stuff in to code
<infinisil>
gchristensen: Have you done anything with formal verification?
<gchristensen>
yeah, a bit
<infinisil>
The type is the specification, so if you get the type right, the compiler enforces the specification in the implementation
<infinisil>
And because idris has such a powerful type system, you can have very complex specifications be enforced
<gchristensen>
right
<andi->
what makes writing types less error prone then writing code?
<__monty__>
They're more abstract.
<infinisil>
andi-: Yeah that's another problem, but arguably an easier one than how to make sure you don't code errors
<infinisil>
(where code = implementation)
<simpson>
Nothing makes it less error-prone, really; but keep in mind that, in practice, one writes the types *and* the expressions, both next to each other, so that the expressions have the given types. This interlocking nature maybe reduces errors.
<gchristensen>
double-entry development seems good
<gchristensen>
but Idris lets you skip writing the implementation
<manveru>
for me the cool part is that you can generate half of your code from the type in idris :)
<andi->
(I am not arguing types are good/bad just wanted to see your arguments :-))
<infinisil>
gchristensen: Eh, it works sometimes, but for more sophisticated types, the algorithm for writing the implementation quickly falls short
<gchristensen>
gotcha
<infinisil>
It probably can't write a sorting algorithm
<samueldr>
we only need two types, files and strings *looks at bash*
<gchristensen>
hell yeah
<infinisil>
gchristensen: I hope that some time in the future, we can use very precise (dependent) types to write production software, while offloading the work of writing and implementing these types to people who know how to do that
<infinisil>
Maybe libraries should implement these things, making them as general purpose and safe for everybody to use
<infinisil>
Such that everybody using these libraries can profit from them, without having to learn about how it's implemented
<infinisil>
With current Haskell I can't say this is working very well, because libraries written with this thought often take forever to figure out how you can even use them..
<__monty__>
Imo types *are* easier to write correctly than code. Less ways to go wrong. +, -, *, /, all the same type but different code.
<__monty__>
Also, most people like the safety Int vs String gives for example, catches simple typos like accidentally swapping arguments. Dependent types let you do things like give sorting algorithms a type from any list to an *ordered* list. If you mess up your algorithm too badly the typechecker'll tell you.
<infinisil>
Yeah
<__monty__>
For some reason people tend to shrug when I mention the `sort :: List -> OList` type. Somehow they don't care almost any library function could just be a blatant lie.
<__monty__>
This point about Blodwen surprises be tbh: Better type checker implementation which minimises the need for compile time evaluation.
<__monty__>
Don't you want *more* compile-time evaluation for performance?
<infinisil>
__monty__: Also note that `sort :: List -> OList` could also lie about it being a sort. It could just return [], which is an ordered list :P
<__monty__>
True but you can include more proof if you want.
<__monty__>
That's too much for the average person that wants to hear an elevator pitch on dependent types though.
Myhlamaeus has quit [Ping timeout: 250 seconds]
<__monty__>
Maybe linear types could help with this? If *every* element of the input needs to be used exactly once...
<__monty__>
I don't know how they mix with dependent types though.
<infinisil>
__monty__: And about the blodwen thing, not sure, I don't know the details, but idris has lots of trouble with compilation times with Nat's, such as demonstrated here: https://github.com/sbp/idris-bi#motivation
<__monty__>
I wonder why he's targetting scheme now. Is haskell a bad fit because of laziness or something?
<infinisil>
I think it's just because it's simpler to start out with
<infinisil>
Code generation is annoying, and using scheme probably makes it a bit less annoying
<__monty__>
Yeah, I guess S-expressions are easier to generate. Though I'd assume some of GHC's intermediate types are more amenable to generation.
<infinisil>
__monty__: I think I remember seeing an implementation of a "UList" somewhere with linear types, which is like a normal list, but every element has this "1" annotation. Then sort could probably just be `sort :: UList -> (out: UList, isSorted out)`
<infinisil>
(Or to be more exact, `sort :: UList n elem -> (out : UList n elem ** IsSorted out)`)
<__monty__>
Cool, need to look into that.
<__monty__>
Have a nice day, everyone.
__monty__ has quit [Quit: leaving]
<elvishjerricco>
uh. If I press ctrl at all, my browser window zooms in
<elvishjerricco>
Getting this constantly in xev:
<elvishjerricco>
ButtonRelease event, serial 30, synthetic NO, window 0x2000001,
<elvishjerricco>
root 0x1e0, subw 0x0, time 465421, (1488,646), root:(1503,1599),
<elvishjerricco>
state 0x10, button 6, same_screen YES
<samueldr>
got a mouse in a bag? got something sitting on a keyboard with funny mouse scrolling support?
<samueldr>
touchpad acting funny?
<elvishjerricco>
samueldr: Only peripherals plugged in are a monitor, external hard drive, speakers, keyboard, and mouse. Unplugging any of them doesn't help
<elvishjerricco>
oh and there's an associated ButtonPress event for that ButtonRelease event
<samueldr>
remote control software on the computer? e.g. synergy or vnc
thePirateKing has quit [Quit: Leaving]
<elvishjerricco>
None that I'm aware of
<samueldr>
otherwise then I'd start looking for ghosts :/
<elvishjerricco>
it persisted past a reboot
<samueldr>
(going through my usual checklist of weird inputs)
<elvishjerricco>
wait... Usually when focus switches from the xev window to my browser, it stops printing those events, and the browser will zoom if i press control. Right now, the browser is focused, but the zoom thing doesn't happen and xev is still printing those events...
<elvishjerricco>
Oh. The signal only comes from the window that the mouse last focused on....
<elvishjerricco>
s/comes from/goes to/
drakonis has joined #nixos-chat
<elvishjerricco>
Oh, I'd only tried turning the mouse off, not unplugging it. Moving it to a new USB port has fixed it. Let's see if I move it back...
<elvishjerricco>
Well it's gone now. Even after a reboot. Blame bad hardware, or get paranoid? :P
<samueldr>
weird state of the usb dongle, most likely
<samueldr>
was it from after a suspend?
<clever>
temporarily taking a break from a proper electron package in nix, and just doing an impure build in ubuntu
ericnoan has quit [Ping timeout: 264 seconds]
ericnoan has joined #nixos-chat
<ldlework>
drakonis: did you see that video
<elvishjerricco>
samueldr: No. Don't think so anyway.
<drakonis>
there's a bunch of mods being created for it
<drakonis>
it
<drakonis>
will have more mods in the future, in a official manner as well
jasongrossman has joined #nixos-chat
<drakonis>
its beautiful
<drakonis>
i wanna play pvp ror2
<ldlework>
have you played 16? its so nuts
jackdk has joined #nixos-chat
<infinisil>
Lol: "One might say it’s opinionated software. Since my opinions are correct, this makes honk the world’s first provably correct social media application."
<joepie91>
"If your post is expected to have some nontrivial lifetime, I think it’s better suited for a blog or such. honk isn’t the best option for that. I associate low friction with low effort. "
<joepie91>
why do people keep making this mistake of conflating 'low barrier' with 'short lifetime' :(
<joepie91>
I really want a thing that lets me write low-effort posts and then 'graduate' them to long-lived posts when they end up organically growing to be bigger / more serious than I anticipated
<gchristensen>
I agree, more people should make them short lifetim