by

Where communities thrive


  • Join over 1.5M+ people
  • Join over 100K+ communities
  • Free without limits
  • Create your own community
People
Repo info
Activity
  • May 01 16:39
    yairchu commented #111
  • May 01 16:17
    danra edited #111
  • May 01 16:17
    danra opened #111
  • Apr 24 17:55

    yairchu on master

    Fix animation of list evaluatio… (compare)

  • Apr 24 14:01

    yairchu on master

    Oops caching sugar broke switch… (compare)

  • Apr 24 12:57

    yairchu on master

    calculate completions in monad … (compare)

  • Apr 23 17:03

    yairchu on master

    Control.Monad.Once: Execute act… Sugaring result is cached Towa… (compare)

  • Apr 23 16:48

    yairchu on wip-cache

    Control.Monad.Once: Execute act… wip (compare)

  • Apr 23 15:44

    yairchu on wip-cache

    Control.Monad.Once: Execute act… wip (compare)

  • Apr 23 15:39

    yairchu on wip-cache

    wip (compare)

  • Apr 23 14:00

    yairchu on wip-cache

    Control.Monad.Once: Execute act… wip (compare)

  • Apr 23 13:56

    yairchu on master

    inline expr (compare)

  • Apr 23 12:07

    yairchu on master

    GUIMain.make gets mkWorkArea pa… (compare)

  • Apr 23 11:15

    yairchu on wip-cache

    Control.Monad.Once: Execute act… wip (compare)

  • Apr 23 10:17

    yairchu on master

    inline function with bad name … minor cleanups (compare)

  • Apr 23 09:37

    yairchu on wip-cache

    Control.Monad.Once: Execute act… wip (compare)

  • Apr 23 09:20

    yairchu on master

    CodeEdit gets the sugared worka… (compare)

  • Apr 23 09:02

    yairchu on wip-cache

    Control.Monad.Once: Execute act… wip (compare)

  • Apr 22 09:26

    yairchu on wip-cache

    Control.Monad.Once: Execute act… wip (compare)

  • Apr 21 22:10

    yairchu on master

    sugarWorkArea does sugaring wor… (compare)

Eyal Lotem
@Peaker
Great! Lamdu is a native app - so the frontend/backend are internal modular divisions. Type editing is currently waiting on a change we're doing to how ASTs are represented, that would allow annotating each subterm in the type-level. These annotations will be used to give identities to subterms so tracking diffs is at a fine-grained level that is easy to later merge (with structural revision control)
For type editing:
1) Our Type AST needs to support annotations -- this item is almost complete.
2) Type sugaring needs to annotate with actions to do the edits, including "type holes" which are like value holes, for editing an incomplete type
3) In the GUI, we need to expand TypeView to TypeEdit, that uses these actions
4) Add "Nominal Type Edit" panes in addition to the REPL pane and definition-edit panes
Janus Troelsen
@ysangkok
reimplemented factorial in current master https://imgur.com/a/Hx8TEpZ :D
congrats on completing the transition to syntax-tree
Eyal Lotem
@Peaker
Thanks! :)
We're making nice progress on translations, hopefully we can release that soon
https://i.imgur.com/l5itWIr.png intermediate state, translation support for Hebrew
Zac Garby
@zac-garby
Hi, this project looks really cool! It said about designing the website - I'd be happy to do that if nobody else has started on that already.
Yair Chuchem
@yairchu
Hi @zac-garby , that could be great!
Zac Garby
@zac-garby
Cool! I have an exam in a couple of hours but I’ll get started later today
Zac Garby
@zac-garby
Is there a high-quality SVG of the logo?
Yair Chuchem
@yairchu
I'm afraid there isn't. We're not graphic designers and the logo is something I whipped up using Pixelmator..
Here's a larger version https://pbs.twimg.com/profile_images/649596775108608000/9V_Xn80d_400x400.jpg
Zac Garby
@zac-garby
ah okay, it's just for the header of the website. i could recreate the circle with the lambda in the middle using CSS, that might look quite cool.
Zac Garby
@zac-garby
Screenshot 2019-05-24 at 18.16.51.png
thoughts?
Yair Chuchem
@yairchu
It does look nice! :) But in when making the current logo, with my non-professional design choices, I felt like just the letter lambda and not much more would be too simple. That's why the logo depicts something akin to Batman's "Bat Signal", i.e "Lambda to the rescue!", which is more specific than just the letter, though perhaps my visual design doesn't really make it clear..
Zac Garby
@zac-garby
Yeah I definitely agree, I like the “bat signal” idea, it’s a bit tricky to do with css though. I’ll probably end up making an svg for it
Yair Chuchem
@yairchu
I like really that gradient for the header :)
Zac Garby
@zac-garby
Thanks :smile:
btw, which font was used for the logo?
Yair Chuchem
@yairchu
Screen Shot 2019-05-24 at 21.24.01.png
Looks like maybe it's a hand-drawn shape..
But I don't think we're attached to the exact "font" :)
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.