btw, which font was used for the logo?
Looks like maybe it's a hand-drawn shape..
btw here's the Pixelmator file https://www.dropbox.com/s/8esu78j2lgstkip/lamdu%20temporary%20logo.pxm?dl=0
But I don't think we're attached to the exact "font" :)
i made a few. the left two are different formats of the logo and the right one is for the website
Btw, Lamdu now has I18N support! https://www.reddit.com/r/lamdu/comments/bugopu/weekly_progress_report_of_20190529/
In latest
And if you know another natural language well it's easy to add more languages!
In latest
master you can switch from coding in English and Hebrew!And if you know another natural language well it's easy to add more languages!
Exciting new feature in Lamdu: you can "insist" on a type mismatch and the mismatch gets pushed elsewhere. so if I have
Btw we're not sure what's the best term to coin for this feature.
if x: 5 else: <"hello"> (angle brackets mark mismatch) I can press space on the <"hello"> fragment and it becomes if x: <5> else: "hello" .Btw we're not sure what's the best term to coin for this feature.
@zac-garby Your logos look great! I especially like the first, simple one. I think the logo can be a simple letter with barely any visual id around it. Consider the facebook logo
Quash fragment, Overrule, Stomp, Contend, Affirm
(all do not have contradicting connotations)
I am working on a dependently typed language, and I think proof assistants is in a position that structual editor is ideal for and much needed, because mathematicians love their LaTeX symbols. As I think more and more about structural editors, I think the semantics of it should be seperated from syntax. so no "semantically bug-free editing", but only that it creates a AST that is type-correct (ast's type in host language). I looked into MPS and found it has very good architecture, but I don't like the way it handles semantics. I think a structural editor framework should be more like language server and only handles editing and presentation.
does this sounds reasonable to you? another structual editor framework?
https://www.youtube.com/watch?v=viF1bVTOO6k&feature=youtu.be this videos applies so much for proof assistants, they usually needs to show the context (type of holes) and also they usually has a open-term evaluator (evaluation with type errors)
Hi! I definitely agree that structural editors and rich IDEs are very suitable for proof assistants, and making a framework for those is certainly useful. But that's a pretty grand task and our focus in Lamdu for now is creating a single language and environment.
Where we can we try to apply good software engineering principles so we try to make our components as re-usable as we can and hopefully other folks could re-use them for other environments :)
Part of our endeavour is that we needed to create a custom UI library for our needs (which are keyboard based editing of rich structures with responsive layout and animations), and coming up with the right design and implementing the UI framework was pretty difficult. The UI library is re-usable btw an we plan to take it out from the Lamdu repo to a standalone library
The way it "is supposed to work" is that it will start laying out the top-level AST nodes vertically so you'll have a lot of
"""
1
+
1
+
1+1+1+1+1...
"""
stuff going on.
"""
1
+
1
+
1+1+1+1+1...
"""
stuff going on.
I asked around and found out the paper I mentioned has a "horizontal compose" operator, and I don't really need this. A simpler one is "wadler's prettier printer," which doesn't have the horizontal compose, and is quite simple and clean. But I think they doesn't quite applies to Lamdu, as it has mixed vertical expression inside horizontal ones.
I haven't decided if I want inline vertical expressions, but I think I tend to make things as close to textual as possible.
In other words: for Lamdu, the optimal layout may not be ideal - as it may be chaotic: change too much between small incremental edits.
Also: Wadler's pretty printer, IIRC, prefers to split vertically as late as possible, so you get lots of tiny trees hanging at the end of a horizontal line.
We prefer the opposite: split vertically as early as possible (in the outer-most expression), and have the lower levels of the AST fit together horizontally in lines.
I've started a little bit with the project, it supports a generic syntax for specifying grammars. here it's the own grammar specified in it's own grammar... it has auto-layout. but I think I have some design problems reguarding baseline alignment when expressions have different hight
I don't know if anyone interested in collaborating on this project...
@molikto if you want to reach a wider structural editing audience you can try in https://www.reddit.com/r/nosyntax/
@ysangkok sorry for the late reply, I missed the notification. Unfortunately we haven't yet implemented editing of nominal types. Did a lot of prep to it so it will come :) You can still import them via a json file and can still of course use structural types