Where communities thrive


  • Join over 1.5M+ people
  • Join over 100K+ communities
  • Free without limits
  • Create your own community
People
Repo info
Activity
  • Jan 25 17:28
    gvnnz closed #115
  • Jan 25 17:28
    gvnnz commented #115
  • Jan 25 10:25

    yairchu on master

    add failing test Fix red cursor when changing ta… (compare)

  • Jan 25 07:42
    yairchu commented #115
  • Jan 24 20:48
    gvnnz opened #115
  • Jan 21 22:07

    yairchu on master

    Add failing test for punned fie… Fix punning of auto-named varia… (compare)

  • Jan 21 20:53

    yairchu on wip

    Add failing test for punned fie… wip (compare)

  • Jan 21 20:07

    yairchu on master

    Remove redundant parameter (compare)

  • Jan 21 19:23

    yairchu on wip

    Add failing test for punned fie… wip (compare)

  • Jan 21 12:06

    yairchu on wip

    Add failing test for punned fie… wip (compare)

  • Jan 21 11:44

    yairchu on master

    minor cleanups (compare)

  • Jan 20 19:42

    yairchu on master

    Use Compose Remove special case in emplace … (compare)

  • Jan 20 18:48

    yairchu on master

    Add failing test for new tag re… Fix failing test and regression… (compare)

  • Jan 20 13:43

    yairchu on alt

    Remove hole extra results: UI s… (compare)

  • Jan 20 13:37

    yairchu on master

    Remove unused exts (compare)

  • Jan 20 11:36

    yairchu on master

    dont pass redundant parameter (compare)

  • Jan 20 11:10

    yairchu on ux-redo

    replaceOptions wip (compare)

  • Jan 20 10:47

    yairchu on ux-redo

    Temporary broken state: Removed… (compare)

  • Jan 20 10:37

    yairchu on master

    Group TH boilerplate lines toge… (compare)

  • Jan 20 10:09

    yairchu on ux-redo

    Temporary broken state: Removed… (compare)

Zac Garby
@zac-garby
hmm ok. well i'll use the default font for now (which is actually arial, yuck), but it's easy to change if we need to.
Zac Garby
@zac-garby
Screenshot 2019-05-24 at 19.36.43.png
i made a few. the left two are different formats of the logo and the right one is for the website
Yair Chuchem
@yairchu
Nice :)
Yair Chuchem
@yairchu
Btw, Lamdu now has I18N support! https://www.reddit.com/r/lamdu/comments/bugopu/weekly_progress_report_of_20190529/
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!
Yair Chuchem
@yairchu
Exciting new feature in Lamdu: you can "insist" on a type mismatch and the mismatch gets pushed elsewhere. so if I have 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.
Yair Chuchem
@yairchu
(new repo to plan scripts for videos and other types of posts. Help wanted from anyone who's good at writing and creating content!)
Eyal Lotem
@Peaker
awesome stuff, @yairchu ! :-)
@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
Zac Garby
@zac-garby
Thanks :) I’ll upload the svgs here tomorrow. I haven’t made much progress on the website, since I’m in the middle of my a-levels at the moment.
Eyal Lotem
@Peaker
@yairchu About the new type feature, some potential names:
Quash fragment, Overrule, Stomp, Contend, Affirm
(all do not have contradicting connotations)
Eyal Lotem
@Peaker
Minghao Liu
@molikto
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?
Minghao Liu
@molikto
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)
Yair Chuchem
@yairchu

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 :)

Minghao Liu
@molikto
I am not sure I am up to such an endeavour yet. as a dependent typed language is already a huge one. what's the hardest part (parts) of the GUI side of lamdu?
Yair Chuchem
@yairchu
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
Minghao Liu
@molikto
what about automate layouting? I just tried with Lamdu and it seems it cannot handle a long expression of 1 + 1... + 1..
Yair Chuchem
@yairchu
what do you mean by "cannot handle"? perhaps you mean you don't like the way it handles it?
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.
Minghao Liu
@molikto
yes. this is not what I expected because in a text editor it softwrap, but again if you are thinking in ASTs what Lamdu do is reasonable.
Yair Chuchem
@yairchu
Yeah, 1+1+1+1+1 is sort of an edge case but the results we get for typical ASTs are quite satisfactory imho
Minghao Liu
@molikto
I am reading the paper "A New Approach to Optimal Code Formatting" and want to see if it fits a projectional editor, but I found that algorithm very cool
Yair Chuchem
@yairchu
Sound interesting I'll have a look at it
Minghao Liu
@molikto
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.
Yair Chuchem
@yairchu
Btw one reason not to go very fancy in an editor's auto layout is that you don't want things to change too much when the users are making edits
Eyal Lotem
@Peaker

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.

Minghao Liu
@molikto
thanks!
Minghao Liu
@molikto
7B2C161CB9CD7DA7497DBACC07B29637.png
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...
Yair Chuchem
@yairchu
@molikto if you want to reach a wider structural editing audience you can try in https://www.reddit.com/r/nosyntax/
Minghao Liu
@molikto
Thanks!
Janus Troelsen
@ysangkok
@yairchu is it possible to define your own types in lamdu now?
Vladimir Gordeev
@vladimir-vg
Hey everyone! Do I understand correctly that Lamdu stores source code as structured data, in database?
Yair Chuchem
@yairchu
@vladimir-vg Yes
@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
Janus Troelsen
@ysangkok
@yairchu nice, i am very excited :) lamdu is such a great project, and you have done great work so far
Fritz Feger
@fritzfeger
Hi there, I just stumbled upon Lamdu and played around with it - great work! It's quite in here... still at it?
As for the relationship between Lamdu and Haskell: do you plan to build some kind of interoparability? Like using Haskell libraries in Lamdu, or transpiling Lamdu to Haskell, "export as Haskell"? What do you think of the latter idea, i.e. of Lamdu as a tool to develop Haskell?
Yair Chuchem
@yairchu
Hi @fritzfeger ! It is indeed somewhat quiet.
2020 has some unexpected turns and both me and Eyal needed to spend time on other things.. But I'm back to spending time on Lamdu since recently!
Yair Chuchem
@yairchu
I'm not sure about interop with Haskell specifically as an early priority, we'll probably want interop with C first
Haskell comes with a set of complications with pervasive lazyness, whereas we choose to go with explicit lazyness
janus.troelsen
@janus.troelsen:matrix.org
[m]
what are nominal types? are they product types, like records?
janus.troelsen
@janus.troelsen:matrix.org
[m]