--- Day changed Fri Mar 10 2017
subttleglguy: Hi, I hate to bother you but is there any chance you still have the video for this? http://blog.ezyang.com/2010/06/well-founded-recursion-in-agda/ 10/03 00:54
gallaiswas it ever made available?10/03 01:14
subttlegallais: there is a link to the video but it's broken, so I tried to manually find it but that page doesn't have the video 10/03 01:18
subttlehttps://galois.com/blog/2010/06/tech-talk-introducing-well-founded-recursion/10/03 01:18
glguyI'll check10/03 01:19
glguyhttps://vimeo.com/3651923410/03 01:20
subttleglguy: many thanks!10/03 01:20
subttleahaha wow, so many questions being asked in this video!! I supposed that is good that they want to understand, but as an audience member there comes a time when you should let the presenter move on for the sake of everyone else and hope the presenter can address your questions personally after!!10/03 02:06
subttleat least it's productive discussion though :D10/03 02:10
subttlebut anyway, this is exactly what I needed, so I am thankful you had it available... I'll shut up now :)10/03 02:11
rntzis agda's termination checker smart enough to know that "subst" doesn't change the size of its argument?10/03 06:18
rntzif not, what's the standard way to get around this?10/03 06:18
rntz(if I need to change the type of the argument I'm inducting on by using subst)10/03 06:18
rntzhm, looks like using "rewrite" can fix it10/03 06:27
rntz... nope, I forgot to take NON_TERMINATING off10/03 06:27
rntzthat's very frustrating10/03 06:35
{AS}rntz: consider using sized types10/03 06:43
{AS}rntz: and perhaps make a sized version of subs10/03 06:43
{AS}subst10/03 06:43
rntz:/10/03 06:47
{AS}rntz: 10/03 06:59
{AS}https://www.irccloud.com/pastebin/al8q0eud/10/03 06:59
{AS}rntz: but I guess maybe the ordinary version of ssubst work when you just use a sized type :)10/03 07:00
akr[m]gallais: how do I define even on sized streams?10/03 11:16
akr[m]agda keeps complaining about being unable to resolve size constraints10/03 11:16
gallaiswhat's even?10/03 11:20
akr[m]https://agda.readthedocs.io/en/latest/language/coinduction.html10/03 11:20
akr[m]like here10/03 11:20
lpaste_gallais pasted “even” at http://lpaste.net/35338010/03 11:23
gallaisakr[m]: even is not size respecting so I'd say something like this ^10/03 11:23
akr[m]ah, interesting10/03 11:25
akr[m]I have to read up on sized types10/03 11:25
akr[m]thank you, that works10/03 11:25
apostolisDoes anyone use the nixos os? Emacs is failing to see the standard lirary.10/03 18:22
qmmapostolis: #nixos10/03 18:56
qmmi imagine that channel would be able to provide help quicker :)10/03 18:57
apostolisqmm : I doubt it :) too few people using agda.10/03 18:59
mudriapostolis: I use NixOS.10/03 20:01
apostolismudri : How did you install agda? I just installed nixos for the first time.10/03 20:03
mudriapostolis: let me have a look...10/03 20:03
apostolisDoes it work with agda-stdlib? take your time.10/03 20:04
mudriHave you done anything so far?10/03 20:04
mudriAnd yeah, I use stdlib from nixpkgs.10/03 20:04
apostolisI put haskellPackages.Agda and AgdaStdlib into my config.nix10/03 20:04
apostolisthen I did emacs-mode setup and emacs-mode compile.10/03 20:05
apostolisThe second failed.10/03 20:05
apostolisemacs does not see the library.10/03 20:05
mudriagda-mode, rather than emacs-mode?10/03 20:06
apostolisyes, sorry :)10/03 20:06
gallaishave you done this: https://agda.readthedocs.io/en/v2.5.2/tools/package-system.html ?10/03 20:06
mudriDid you carry any of your Agda config over from your last distro?10/03 20:07
apostolismudri : No.10/03 20:08
mudriOkay. It probably wouldn't help too much, anyway.10/03 20:08
apostolisgallais : This is too complicated. I did not.10/03 20:08
apostolisgallais : Or I could say that it is not very clear.10/03 20:09
mudriIn agda2-program-args, I have "--include-path=." and "--include-path=/home/uname/.nix-profile/share/agda/".10/03 20:09
apostolisI installed agda from the main config.nix, not as a user.10/03 20:10
gallaisapostolis: just create .agda/libraries with one line "/PATH/TO/AGDA_STDLIB/standard-library.agda-lib"10/03 20:10
apostolisMy .profile is empty.10/03 20:10
mudriYou mean /etc/nixos/configuration.nix?10/03 20:10
apostolismudri : Yes.10/03 20:10
apostolisgallais : That is simpler/10/03 20:11
gallaisit's literally what the doc is saying10/03 20:11
mudriThe equivalent is /run/current-system/sw/share/agda/"10/03 20:12
apostolisgallais : It is intermingled with how to create your own library If I remember correctly.10/03 20:14
apostolismudri : Let me try it. Need to reinstall the library. I was trying to compile it.10/03 20:15
mudriMaybe I should try the library thing at some point.10/03 20:16
gallais"Before we go into details, here is some quick information for the impatient on how to tell Agda about the location of the standard library, using the library management system."10/03 20:16
apostolisOk i am going to restart the computer, I cannot find the stdlib where mudri pointed.10/03 20:28
mudriapostolis: by the way, I have Agda installed using ghcWithPackages. I don't know whether that makes a difference, but I would guess not.10/03 20:29
apostolismudri : Have you tried compiling Agda? cabal cannot find some include files like zlib.h10/03 20:31
apostolisWhere does nixos keep them? I have installed the zlib library.10/03 20:32
mudriapostolis: no. You'd probably have to have a relevant .nix file to make it do anything.10/03 20:32
mudriDoes agda not have a .nix file?10/03 20:32
apostolisIt does not seem like it.10/03 20:33
apostolisOnly agda-stdlib has one I think.10/03 20:33
mudriBut Haskell in Nix is incredibly overengineered. There are about 7 different ways to build a Haskell project on NixOS.10/03 20:34
mudriDo you need to compile a non-release version?10/03 20:34
apostolisI would really prefer to use the agda master.10/03 20:35
apostolisrebooting ...10/03 20:36
mudri|srcfWhere'd he do?10/03 21:03
mudri|srcfs/do/go/10/03 21:03

Generated by irclog2html.py 2.7 by Marius Gedminas - find it at mg.pov.lt!