Closed yurrriq closed 7 years ago
@yurrriq, this is a very nice initiative! Certainly something I'd love to contribute to. I'm about half way through SF-in-Coq so contributing here would help motivate me complete SF-in-Coq while working out how to do all this stuff in Idris.
A quick google search seems to indicate that GFM = GitHub Flavoured Markdown?
Might be nice to set up a Gitter channel for this project (if you don't mind that kind of thing).
Awesome! I don't have much experience with Gitter but would be amenable to it. Maybe @jfdm has to set it up since he's the admin.
Is there a chance for the Gitter channel to happen? I'm almost done with Poly
and anticipate getting stuck on the coming chapters - would be cool to have a place to ask for help and invite potential contributors to.
I have no experience setting that up and don't use Gitter, personally. I'm yurrriq on IRC and hang out in #idris. Feel free to mention or DM me there whenever.
To avoid duplicated efforts could you open issues or WIP PRs when you're working on new stuff so I and others know what not to do?
You're more likely to get ahold of Idrisers on #idris on Freenode -- Gitter isn't big in the Idris community.
@david-christiansen Sure, my idea was to have some dedicated place to discuss SF-related issues and not to flood the main channel. The book does ask not to post solutions in public after all :) But I guess this won't generate much traffic, so it's probably safe to discuss directly in #idris or ##dependent.
I don't think anyone would mind discussion of writing Idris on #idris. Clearly, you should feel free to discuss things wherever you want --- I just figure you're likely to encounter general Idris issues that the folks in #idris can help with, and that this might be useful.
I think Coq and Idris are different enough too that we wouldn't be ruining much for any Coq students by discussing strategies in Idris.
TODO
shell.nix
sorted (TeX in Nix is pretty broken atm...)pandoc
workflow, including the hybrid GFM/TeX Literate Idris.Consider ditching the hybrid GFM madness for regular LaTeXThis turned out to be more annoying that it seemed worth, so I abandoned the idea.