Guest57308 Guest57308 Guest57308 --- Day changed Mon Jan 15 2018 Текст ниже запросил awesomelackware. 15/01 09:48 ТЫ БОЛЕН, ПОЭТОМУ ЛЕЧИСЬ! 15/01 09:48 ГОВНО ТЫ 15/01 09:48 САМ ТЫ ШИЗИК! 15/01 09:48 ИДИ ДАЛЬШЕ 15/01 09:48 ТЫ БОЛЕН, ПОЭТОМУ ЛЕЧИСЬ! 15/01 09:48 ТЫ БОЛЕН, ПОЭТОМУ ЛЕЧИСЬ! 15/01 09:48 САМ ТЫ ШИЗИК! 15/01 09:48 ЗАКРОЙ РОТ 15/01 09:48 ЗАКРОЙ РОТ 15/01 09:48 Я НЕ ШИЗИК 15/01 09:48 Текст ниже запросил awesomelackware. 15/01 09:49 Я НЕ ШИЗИК 15/01 09:49 ТЫ БОЛЕН, ПОЭТОМУ ЛЕЧИСЬ! 15/01 09:49 ГОВНО ТЫ 15/01 09:49 ТЫ БОЛЕН, ПОЭТОМУ ЛЕЧИСЬ! 15/01 09:49 ИДИ ДАЛЬШЕ 15/01 09:49 САМ ТЫ ШИЗИК! 15/01 09:49 Я НЕ ШИЗИК 15/01 09:49 ГОВНО ТЫ 15/01 09:49 ССУ ТЕБЕ В ЛИЧКУ! 15/01 09:49 ГОВНО ТЫ 15/01 09:49 awesomelackware: заебал, не сри здесь, дебил. 15/01 09:49 Bratishka, иди нахуй 15/01 09:49 Sorry guys, He is just stupid F#-lover 15/01 09:49 Sorry guys 15/01 09:49 Bratishka is stupid Scala user 15/01 09:49 F# > Scala 15/01 09:54 jfdm, 卐 15/01 10:40 twanvl, ты хуй 15/01 10:54 бля 15/01 10:54 ГЕИ 15/01 10:54 ШИЗИКИ 15/01 10:54 ШИЗИКИ 15/01 10:54 ШИЗИКИ 15/01 10:54 ШИЗИКИ 15/01 10:54 ШИЗИКИ 15/01 10:54 ШИЗИКИ 15/01 10:54 ШИЗИКИ 15/01 10:54 ШИЗИКИ 15/01 10:54 ШИЗИКИ 15/01 10:54 ШИЗИКИ 15/01 10:54 ШИЗИКИ 15/01 10:54 ШИЗИКИ 15/01 10:54 ШИЗИКИ 15/01 10:54 ШИЗИКИ 15/01 10:54 ГЕИ 15/01 10:54 ГЕИ 15/01 10:55 ГЕИ 15/01 10:55 ГЕИ 15/01 10:55 ГЕИ 15/01 10:55 ГЕИ 15/01 10:55 ГЕИ 15/01 10:55 ГЕИ 15/01 10:55 ГЕИ 15/01 10:55 ГЕИ 15/01 10:55 ГЕИ 15/01 10:55 ГЕИ 15/01 10:55 ГЕИ 15/01 10:55 ГЕИ 15/01 10:55 ГЕИ 15/01 10:55 ГЕИ 15/01 10:55 ГЕИ 15/01 10:55 ШИЗИКИ 15/01 10:55 ШИЗИКИ 15/01 10:55 ГЕИ 15/01 10:55 ШИЗИКИ 15/01 10:55 ШИЗИКИ 15/01 10:55 ШИЗИКИ 15/01 10:55 ШИЗИКИ 15/01 10:55 ШИЗИКИ 15/01 10:55 ГЕИ 15/01 10:55 ГЕИ 15/01 10:55 ГЕИ 15/01 10:55 ГЕИ 15/01 10:55 ГЕИ 15/01 10:55 ШИЗИКИ 15/01 10:55 ШИЗИКИ 15/01 10:55 ШИЗИКИ 15/01 10:55 ШИЗИКИ 15/01 10:55 ШИЗИКИ 15/01 10:55 ШИЗИКИ 15/01 10:55 ШИЗИКИ 15/01 10:55 ШИЗИКИ 15/01 10:55 ШИЗИКИ 15/01 10:56 ШИЗИКИ 15/01 10:56 ШИЗИКИ 15/01 10:56 ШИЗИКИ 15/01 10:56 ШИЗИКИ 15/01 10:56 ШИЗИКИ 15/01 10:56 ШИЗИКИ 15/01 10:56 ШИЗИКИ 15/01 10:56 ШИЗИКИ 15/01 10:56 ШИЗИКИ 15/01 10:56 ШИЗИКИ 15/01 10:56 ГЕИ 15/01 10:56 ГЕИ 15/01 10:56 ГЕИ 15/01 10:56 ГЕИ 15/01 10:56 ГЕИ 15/01 10:56 ГЕИ 15/01 10:56 ГЕИ 15/01 10:56 ГЕИ 15/01 10:56 ГЕИ 15/01 10:56 ГЕИ 15/01 10:56 ГЕИ 15/01 10:56 ГЕИ 15/01 10:56 ГЕИ 15/01 10:56 ГЕИ 15/01 10:56 ГЕИ 15/01 10:56 ГЕИ 15/01 10:56 ГЕИ 15/01 10:56 ГЕИ 15/01 10:56 ГЕИ 15/01 10:56 ГЕИ 15/01 10:56 ГЕИ 15/01 10:56 ГЕИ 15/01 10:56 ШИЗИКИ 15/01 10:56 ГЕИ 15/01 10:56 ГЕИ 15/01 10:56 ГЕИ 15/01 10:56 ГЕИ 15/01 10:56 ГЕИ 15/01 10:56 ГЕИ 15/01 10:57 ГЕИ 15/01 10:57 ШИЗИКИ 15/01 10:57 ГЕИ 15/01 10:57 ГЕИ 15/01 10:57 ГЕИ 15/01 10:57 ГЕИ 15/01 10:57 ШИЗИКИ 15/01 10:57 ШИЗИКИ 15/01 10:57 weird bots o.0' 15/01 11:35 just learned that /msg ChanServ access #agda list gives the list of ops of this channel and we just got a new one 15/01 14:21 are you pgiarrusso ? 15/01 14:29 oh mietek is 15/01 14:30 pgiarrusso im trying to define a relational type in which inhabitants need to be a subset of A B, is this possible? 15/01 14:37 Nik05: in type theory it’s easier to encode subsets of S as predicates on members of S (S -> Set), but I think we discussed this? 15/01 14:48 yes 15/01 14:48 is A B a typo for not (A == B) 15/01 14:48 ? 15/01 14:49 is the set cross product from Relation.Unary 15/01 14:49 I’m also not sure on “relational type” and “inhabitants need to be subset”, but are you trying to write data Foo : Set 1 where Bar : (A B -> Set) -> Foo or something such? 15/01 14:50 important bit is that predicates at Set l can only be contained in types at Set (suc l) 15/01 14:51 Nik05: ^^ 15/01 14:51 let me try to explain what i meant 15/01 14:52 Definition 4.2.1. Suppose A and B are sets. Then a set R ⊆ A × B is called a 15/01 14:54 relation from A to B. 15/01 14:54 This is a definition from a book 15/01 14:54 Nik05: (0) the Agda standard library defines what is a relation in Agda, and that’s essentially a binary predicate 15/01 14:55 so a relation on A and B is just a member of type A -> B -> Set 15/01 14:55 ok 15/01 14:55 (1) but you’re correctly noticing that does *not* model the book definition 15/01 14:56 indeed, that book is giving a standard set-theoretic definition, and some set-theoretic concepts need to be modified to be expressed in type theory 15/01 14:56 and this is just another example 15/01 14:57 OTOH, if you want, you can use time A \times B -> Set, it’s equivalent to A -> B -> Set by currying, but as a matter of style often the latter is preferred 15/01 14:58 SO this would be a correct definition: R = Pred A l1 \to Pred B l2 \to Set _? 15/01 14:58 where A and B are the predicate variables 15/01 14:59 Nik05: no, you want R = A -> B -> Set l, or R = A \times B -> Set l, or R = Pred (A \times B) l — they’re all equivalent 15/01 15:40 but then my set isnt a subset of the crossproduct of the two other sets 15/01 15:46 how do i make my predicate depend on the two other predicates? 15/01 15:47 lets say i got the predicate Four = _<_ 4 : Pred Nat zero 15/01 15:49 Now I want a relation between Four and Four, which should be a subset of Four Four 15/01 15:49 Pred (Nat x Nat) zero is too large, because it can also contain (4, 4) 15/01 15:50 But I guess this isnt possible? 15/01 15:52 Or I need to use a record of which one field is a Pred (Nat x Nat) zero and the other field a proof that that predicate is a subset of Four Four. But then I dont have a set anymore 15/01 15:53 Hello. do notation is first in Agda 2.6, right? 15/01 16:50 the official one, anyway https://agda.readthedocs.io/en/latest/language/syntactic-sugar.html 15/01 16:58 mietek: pgiarrusso  i think the folks at #freenode-sigyn have a spam police bot you can get added to a channel 15/01 17:15 akr agda 2.5.4 15/01 17:28 there is not agda 2.6 15/01 17:28 oh, hmm 15/01 17:29 any idea when Arch Linux might get 2.5.4? 15/01 17:30 Nik05: ^ 15/01 17:30 sorry i dont know anything about agda (releases), or Arch 15/01 17:31 nevermind, thanks for clearing up that confusion for me anyway 15/01 17:31 (website says Agda 2.6.0 and doesn't mention 2.5.4) 15/01 17:32 ugh, why is there in the stdlib toNat : Char → ℕ but not fromNat is missing? 15/01 17:33 it is missing, I mean 15/01 17:33 2.6.0 is the codename for master 15/01 17:34 as a rule of thumb, if the stdlib looks incomplete it usually is 15/01 17:34 so what can be done about this 15/01 17:35 fromNat needs to be exported from Agda.Builtin.Char or something 15/01 17:35 at least the Agda stdlib, and if you have looked a bit 15/01 17:35 well, send a PR :-) 15/01 17:36 i mean, primFromNat needs to be exported from there 15/01 17:36 and/or file an issue 15/01 17:36 hmm, I don't really know about this prim / built-in stuff 15/01 17:36 sounds like you're halfway to a fix or at least a good PR 15/01 17:36 can I also remove unnecessary imports? :P 15/01 17:37 if you're saying that you need a new primitive and a patch to Agda, well, that's maybe trickier 15/01 17:38 but same thing 15/01 17:38 I mean, Agda devs are busy people and aren't paid to maintain it for everybody's needs, but they do welcome help and are nice 15/01 17:39 oh, wait 15/01 17:39 primNatToChar is actually exported from Agda.Builtin.Char 15/01 17:39 it's just not re-exported by Data.Char 15/01 17:39 OK, so can you do the PR? 15/01 17:40 (how do you find out what is exported from a module, anyway) 15/01 17:40 yeah 15/01 17:40 if I can manage to clone the repo on train wifi :P 15/01 17:40 otherwise do a edit through GitHub 15/01 17:40 if you can test the change locally it's nicer though, but might save the cloning :-) 15/01 17:41 "do a edit through GitHub" … and not have my code type-checked? you must be crazy :P 15/01 17:42 you have a local copy of the stdlib, no? test it there 15/01 17:42 or do a shallow clone 15/01 17:42 ok, fair point 15/01 17:43 but yes there are trade-offs, and I forget how much CI the stdlib has 15/01 17:43 I think we do have Travis 15/01 17:43 anyway gotta go, but feel free to tag me too in the PR if you do, I'm @blaisorblade 15/01 17:43 sure thing 15/01 17:44 busy, but if the PR is easy enough I could probably approve it 15/01 17:44 thanks for the help :) 15/01 17:44 import cleanups should be separate 15/01 17:44 oh wait, not sure I can commit to the stdlib, but maybe I can still offer a review 15/01 17:44 well, thank you for the PR 15/01 17:45 beware I'm on a phone and I haven't checked the code myself though 15/01 17:45 bbl 15/01 17:45 akr: ^^ 15/01 17:46 I don't know how to make spacemacs ignore my system-wide installation of stdlib :( 15/01 17:51 akr: why do you think it’s a spacemacs thing? 15/01 17:51 akr: what’s in your ~/.agda? 15/01 17:52 well it's just that as a spacemacs user, I don't really know how emacs works :P thought I should mention that 15/01 17:52 akr: either drop the stdlib from ~/.agda/defaults (or such) 15/01 17:52 or maybe you used the old setup in the emacs config, but that was something you had to do by hand 15/01 17:52 if the 2nd case is false, spacemacs is not involved 15/01 17:53 yeah that's the weird thing, I only have .agda/libraries 15/01 17:53 and it doesn't have the stdlib 15/01 17:53 akr: what’s in your ~/.emacs? 15/01 17:53 you don't have that with spacemacs 15/01 17:53 I think it's the doing of the agda spacemacs layer 15/01 17:54 beyond my pay grade 15/01 17:55 anyway, next time there’s spam in the channel, ping comietek 15/01 17:55 hmm, maybe not 15/01 17:55 akr: maybe review customize-group agda-mode? or ~/.spacemacs ? 15/01 17:57 already checked .spacemacs, will try the other thing 15/01 17:58 akr: actually, I’d use ps to check the command line args agda got 15/01 18:00 akr: if it got any, they come from SPC SPC customize-group Agda2 (sorry for the imprecision earlier) 15/01 18:01 OTOH, for this patch it might be faster to reinvoke typechecking from the command line, even though it’s not an ideal workflow 15/01 18:01 hmm ok the include path doesn't come from customize-group 15/01 18:03 I'm guessing this must be an arch-specific thing 15/01 18:06 hmm, even if I force it to look elsewhere with agda --include /dev/null Data/Char/Base.agda it's still finding my system installation of the stdlib 15/01 18:11 --no-libraries doesn't help either 15/01 18:11 weird 15/01 18:11 test with plain emacs? 15/01 18:13 get rid of your system installation of stdlib?  it’s just a git checkout anyway 15/01 18:13 this was running /usr/bin/agda from the command line 15/01 18:13 how are you determining that the stdlib is available? 15/01 18:13 the include path remains and messes stuff up 15/01 18:13 what do you mean? 15/01 18:14 uh.  you’re running agda from the command-line and the include path remains? 15/01 18:14 yeah :/ 15/01 18:14 how can you tell? 15/01 18:14 well, I still get the same error 15/01 18:15 which is what? 15/01 18:15 http://lpaste.net/361665 15/01 18:15 what is the pwd? 15/01 18:16 cwd* 15/01 18:16 /home/osense/dev/agda-stdlib/src 15/01 18:17 what happens when you just do agda Data/Char/Base.agda? 15/01 18:17 then it complains about an ambiguous module name, saying it could be referring either to the system installation of the stdlib or my fork in /home 15/01 18:18 I should've just edited my installation of stdlib in-place 15/01 18:19 stuff is weird 15/01 18:19 what happens when you do agda --no-default-libraries Data/Char/Base.agda? 15/01 18:19 same as one before 15/01 18:20 akr wait no, you might want —include . 15/01 18:24 akr that error is not saying that agda knows about the *stdlib*, it says it knows about the *primitive lib*, which it MUST do 15/01 18:24 I don’t know the official name for what I just called “primitive lib” 15/01 18:24 but recent Agdas install a set of .agda files in some “prim” folder and they’re always available (and in fact, required) 15/01 18:25 that’s where the Agda.Builtin.* modules come from 15/01 18:25 I tried that as well, no luck :| but nevermind, I just edited my system installation of the stdlib and had that type-checked 15/01 18:27 OK good 15/01 18:27 meanwhile, I’m also seeing strange stuff 15/01 18:28 hmm 15/01 18:28 my entire stdlib is in the prim folder 15/01 18:28 I guess that would explain it 15/01 18:29 wat 15/01 18:29 well yeah that sounds broken 15/01 18:29 I guess the package maintainer thought it would be a good idea :D 15/01 18:29 well... actually... it could even be 15/01 18:29 I mean, for the users who *don’t* modify the stdlib, it does simplify the setup 15/01 18:30 because users don’t need to put stuff in their ~/.agda 15/01 18:31 you don't need to deal with setting it up as a library in your ~/.agda 15/01 18:31 it does have some advantages 15/01 18:31 akr: OK, we converged :-) 15/01 18:31 but yeah 15/01 18:31 yeah 15/01 18:31 TL;DR. it’s non-standard but works 15/01 18:32 heh, I'm having a pretty bad delay in my irc client right now 15/01 18:32 ah 15/01 18:32 while for most Haskell packages, the Arch setup is non-standard and *doesn’t* work 15/01 18:32 I don’t use Arch but I’ve seen multiple reports in various forums 15/01 18:32 OTOH, the last interaction we on the Stack side had with the Arch maintainer was helpful — we got them to change something (I forget what) 15/01 18:33 I heard that nix is good for dealing with haskell packages 15/01 18:34 haven't really tried it myself, though 15/01 18:35 I’ve heard it is good and has a steep learning curve 15/01 18:38 I'm going to add all the other stuff into Data.Char.Base that's exported from Builtin.Char, how should I deal with  primCharEquality : Char → Char → Bool ? Should I just re-export it verbatim? 15/01 18:39 and I’m busy enough finishing my PhD :-) 15/01 18:39 akr: uh, not sure there 15/01 18:39 should I try to do something with Decidable? 15/01 18:40 it’d be nice to have actual decidable equality, which is non-trivial to get from that primitive :-| 15/01 18:40 I've only seen it used on Agda-defined datatypes 15/01 18:40 no? 15/01 18:40 wait 15/01 18:40 wait wait 15/01 18:40 have you looked at Data.Char in 0.14? 15/01 18:41 I see a definition of decidable equality 15/01 18:41 https://www.irccloud.com/pastebin/NYnrRS7L/ 15/01 18:42 comietek: Data.Char has something similar 15/01 18:43 just confused because those postulates will make evaluation stuck 15/01 18:44 ah cool 15/01 18:44 this definition worked for me when I was doing names in contexts 15/01 18:45 but it’s probably not ideal 15/01 18:45 mietek: s/similar/alpha-equivalent 15/01 18:46 maybe you took Data.Char as inspiration and forgot 15/01 18:46 akr: seems fromNat is still missing 15/01 18:46 s/still/indeed/ 15/01 18:47 yeah and a bunch of other stuff from Builtin 15/01 18:47 akr: still no clue, but you might want to look into git logs for those files to see if those have a reason for the missing primitives 15/01 18:51 maybe Builtin was updated and the library wasn’t updated yet 15/01 18:51 (which logs would also tell) 15/01 18:51 there's even an import for Bool, which you'd need to the other prim functions which are missing 15/01 18:51 not sure if a PR is faster 15/01 18:51 hmm ok I broke my installation of emacs 15/01 18:52 but looking at logs, while slower, lets you give a superior result 15/01 18:52 > and I’m busy enough finishing my PhD :-) 15/01 18:52 Good luck! 15/01 18:52 did you break it through changes to emacs or through changes to the prim folder? 15/01 18:52 :1:6: error: lexical error at character 'm' 15/01 18:52 damn it lambdabot, we’re not talking to you just quoting stuff 15/01 18:53 I thought that error was the one from akr’s before I looked at the nick O_O’ 15/01 18:53 OK, time to log off and/or sleep and/or study 15/01 18:54 Oh thats a reply to me 15/01 18:54 yep, but happens to me too, all the time 15/01 18:54 O_O’’’  😓😅 15/01 18:54 pgiarrusso: changes to the prim folder, which I subsequently erased 15/01 18:54 Nik05: anyway thanks 15/01 18:54 /usr/share/agda/lib/prim/Data/Char/Core.agdai: openBinaryFile: permission denied (Permission denied) 15/01 18:55 Have a voor evening 15/01 18:55 Good* 15/01 18:55 akr: did you edit it as root and have a restrictive umask? 15/01 18:55 no clue why it's trying to open that file 15/01 18:55 oh well 15/01 18:55 I mean, it does say permission denied 15/01 18:55 well, when it typechecks it tries to write that file 15/01 18:55 hmm, well I did edit it as root 15/01 18:55 unless it’s already up-to-date 15/01 18:55 hmm 15/01 18:56 OK, retypecheck the changed files as root to restore order 15/01 18:56 and check their permissions are right 15/01 18:56 but it doesn't do that when you're just loading that file, I think 15/01 18:56 644 I guess 15/01 18:56 I mean, no other files in the stdlib have an .agdai with them 15/01 18:56 I'm just trying to import Data.Char from my project now 15/01 18:57 akr: was that so earlier? 15/01 18:57 no :) 15/01 18:57 I’d expect all stdlib files to come with their .agdai` 15/01 18:58 but reinstalling the Arch package is safer than reverse-engineering it 15/01 18:59 akr: just confirmed that my prim folder has an agdai file for each agda one, though it’s not using an Arch package — it’s just an Agda installed through stack 15/01 19:00 oh yeah reinstall fixed it 15/01 19:02 thanks :) 15/01 19:02 -!- mode/#agda [+o mietek] by ChanServ 15/01 23:45 -!- mode/#agda [-o mietek] by mietek 15/01 23:46