Where communities thrive


  • Join over 1.5M+ people
  • Join over 100K+ communities
  • Free without limits
  • Create your own community
People
Repo info
Activity
  • Sep 19 01:40

    oeed on develop

    Changed to MIT license (compare)

  • Feb 26 21:37
    jmc529 starred oeed/Silica
  • Feb 23 02:10
    xvxx starred oeed/Silica
  • Nov 05 2019 07:48
    jsgrant starred oeed/Silica
  • Oct 14 2019 01:32
  • Jun 28 2019 18:20
    adamc295 starred oeed/Silica
  • Mar 03 2019 01:37
    ardera commented #26
  • Feb 16 2019 02:37

    oeed on develop

    Update README.md (compare)

  • Feb 16 2019 02:34
    oeed closed #25
  • Feb 16 2019 02:34
    oeed commented #25
  • Feb 15 2019 22:33
    Lemmmy starred oeed/Silica
  • Feb 15 2019 15:29
    SquidDev commented #26
  • Feb 15 2019 14:55
    exerro closed #26
  • Feb 15 2019 14:55
    exerro commented #26
  • Feb 15 2019 14:36
    exerro commented #25
  • Feb 15 2019 14:26
    jojomoore2007 commented #26
  • Feb 15 2019 14:15
    jojomoore2007 commented #26
  • Feb 15 2019 14:14
    jojomoore2007 opened #26
  • Feb 15 2019 14:01
    jojomoore2007 opened #25
  • Feb 07 2019 23:03
    oeed closed #24
hydraz
@plt-hokusai
if you're talking about amulet, you can just set AMC_LIBRARY_PATH to a colon-separated list of paths
Jonathan Coates
@SquidDev
I love that Guix has asdf support baked in as a build system.
Wow, that's actually a massive support list. Kudos.
Drew
@CoderPuppy
Is there a way to run the prebuilt (arch package) portably? I.e. not relying on system paths
oh, that's just a script
hydraz
@plt-hokusai
the library path also contains $(dirname $0)/lib and $(dirname $0)/../lib
so as long as the amc binary itself (/usr/lib/amuletml/amc) is in the same directory as the libraries, or shares a common parent directory with the libraries, you'll be fine
Drew
@CoderPuppy
yeah, the problem was that I was trying to run /usr/bin/amc instead of /usr/lib/amuletml/amc
hydraz
@plt-hokusai
right, /usr/bin/amc is just a wrapper
Drew
@CoderPuppy
Is there any way to extend a record? { { a = 1 } with b = 2 }
hydraz
@plt-hokusai
Amc.extend_row @"b" 2 {a = 1}
Jonathan Coates
@SquidDev
IIRC with b = 2 works right, just only allows updating rather than extending?
Drew
@CoderPuppy
yeah
hydraz
@plt-hokusai
yes
Drew
@CoderPuppy
Where have you been talking about Amulet now?
hydraz
@plt-hokusai
private slack
maybe we should move it somewhere better but gitter is Uhh
Drew
@CoderPuppy
I don't think Gitter has improved (or changed at all) since Silica was active (late 2017?)
Jonathan Coates
@SquidDev
I've just been connecting over IRC, which makes it usable....
I think GitLab brought it, and then did nothing with it?
hydraz
@plt-hokusai
exactly
maybe we should have an amulet irc
Jonathan Coates
@SquidDev
Because the #urn one went so well :)
hydraz
@plt-hokusai
:p
Drew
@CoderPuppy
Have either of you looked at some of the new fancy type theories? Cubical or Quantitative?
Jonathan Coates
@SquidDev
I know Cubical exists, because the Agda people won't shut up about it. That's about the extend of my knowledge - I know hydraz has done more work on this.
hydraz
@plt-hokusai
i've played with cubical agda and read the hott book
i have a wip qtt checker but it is very wip
Jonathan Coates
@SquidDev
Is QTT the one Idris 2 uses?
Drew
@CoderPuppy
Yep
hydraz
@plt-hokusai
yep
Drew
@CoderPuppy
combining linear and dependent types
Jonathan Coates
@SquidDev
Yeah, I really should have remembered this...
Drew
@CoderPuppy
One thing about it that seems interesting is that I think it allows dropping the parametricity of Π(A : Type).
hydraz
@plt-hokusai
i mean, you can already do that with Typeable
or in a dependently typed language, codes for types
Drew
@CoderPuppy
so it might allow typed tactics (a la VeriML) directly in the language
hydraz
@plt-hokusai
i don't like matching on Type
i think matching is for inductive families only and Type is not an inductive family
Drew
@CoderPuppy
I actually found an oddity with that, Agda doesn't support matching on types but they used to make type constructors injective which is similar
they stopped that because someone found a contradiction, but I think that's just because positivity checking wasn't applied to type constructors (because you can't match on them)
Benedict Allen
@exerro
Woah, actually conversation on gitter
InternetUnexplorer
@InternetUnexplorer
Oh hey some activity
I seem to have missed it by a bit, but hello
João Victor
@jv110
hello
João Victor
@jv110
where else can I see you?
Andrew Kvapil
@viluon
Can't wait for the Silica release
@oeed has been working on it for so long, it has to be epic by now
João Victor
@jv110
oof
Jonathan Coates
@SquidDev
What on earth