Week 46: What’s everyone hacking on this week?

Community
21

Apart from mundane maintenance stuff, this week I’m playing even more with the documentation of Genspio.

:construction: Work-In-Progress :construction:

for 2 versions of Genspio:

  • the lib loaded in an OCaml Top-level running in a WebWorker
  • which itself is manipulaed by a Tyxml_js/react mini-webapp.
  • One can download the output of the EDSL compilation as a script.

the whole website itself built with GitLab-CI at every push to master:

https://smondet.gitlab.io/genspio-web-demo/

2 Likes
22

Fork is not always bad. We added built in conditional compilation support and warnings for polymorphic comparison which is something pretty cool

1 Like
23

Barely making it this week.

Adding static generation to Logarion. Copying static files and fixing templating remains.

24

Just submitted some patches to the MacPorts people to update a bunch of moribund OCaml packages. Not a big project but I thought I’d mention.

25

Instead to play with Coq, I played with GADTs. The next goal is to map the ADT with the 1ml lambda ADT, then, the second goal is to produce a malfunction output.

2 Likes
26

Finishing up the last installation of my Ecaml tutorial series. Should be posted later today.

27

@dinosaure: If it’s any use, https://mastodon.social/@freebroccolo/99028229191301715

28

If I understand correctly your code, you have two typed lambda-calculus with base types : one in the module A, and one in the module B. And in the latter you use GADT to enforce well-typed AST. Am I right ?

Are you aware of the Programming Languages Zoo from Andrej Bauer ? There is already a miniml implemented with this framework : presentation on its website. It may be useful to have a REPL for your languages (to play with them) before native-compiled them via malfunction.

Do you mean the ML flavor with core language and module language unified like in this Andreas Rossberg’s paper ?

29

Yeah it could be useful to branch an REPL on the ADT and try to translate the input to the GADT (and compute it) ! I think, it’s not a big deal (just boring lexing and parsing, but I can take plzoo for that).

I would like to branch 1ml from the Andreas Rossberg’s paper :slight_smile: ! Then @anon72795300, I see the initiative of Darin Morison on twitter, but my goal is just for fun (it’s not serious) and I asked before this initiative to Andreas Rossberg to share a github repository to fork it (and keep the [paternity law][^1] of the project).

[1]: maybe I’m wrong on this term.