rawlins/lambda-notebook

Lambda Notebook: Formal Semantics in Jupyter

lambda-notebook's Issues

VSCode (vscode-jupyter) rendering of HTML+latex is broken

VSCode seems to have broken rendering for both latex within HTML and latex within markdown. This affects rendering of trees and formula derivations. See the following issues:

• microsoft/vscode-jupyter#7801
• microsoft/vscode-jupyter#8131 (maybe)
• microsoft/vscode#203725 (maybe)

The situation doesn't look super promising (the main issue has autoclosed) so I have put in a quick error in 2dbe90b so that the user has some idea what's going on. This is really an upstream issue, but it's useful to have an issue here in case people come looking.

Unclear right now if there's any hope of workarounds along the lines of the colab solution. The main idea that comes to mind is to try to find a way to run MathJax(?) manually in HTML outputs, but I don't even know where to begin on this in VSCode.

Windows installation and related issues

I have no experience with this right now (and little access to windows), any feedback would be extremely welcome. Should go like this:

• install python as normal
• install jupyter as normal: http://jupyter.readthedocs.org/en/latest/install.html
  • anaconda
• install lambda notebook into a directory
• then ...
  • python lambda_notebook.py in command prompt in that directory is my best guess
  • can I create a .bat version of the mac command file?
  • need to ensure that whatever it is is run by python3? Should work with python launcher.

Error message improvement

Error messages should generally be better, this issue is for putting down ideas about this.

More fragments

Long-term goal: convert every paper I've written to a lambda notebook fragment.

Solicit fragments from anyone who might be interested.

Test issue 2

try again

Merge identical denotations during composition

Right now, identical denotations are kept as separate composition paths, leading to a combinatorial problem. These should be merged into a single composite that remembers what paths led to it.

Secondary issue: this would work even better with a normal form for the PL subset of the metalanguage.

Real implementation of LF / QR

Need to enhance the syntactic side of TreeCompositionSystems so that things like QR can actually be implemented.

Test issue

testing slack integration

General rendering problems

With current Jupyter, html-css is the only installed renderer, and other renderers are quite challenging to install. Unfortunately, it is slow and ugly for a bunch of crucial lambda notebook cases.

• can the full install be automated to get access to svg? Is mathml better than it used to be?
• bug with renderer selection is fixed in Jupyter trunk.
• can the tree rendering code move away from tables somehow? Note that divs do not fix the issue.
  • Basically, mathjax is not great at predicting what size it will be, and tables/divs need this for layout.
  • gets systematic size undershoots and weird linebreak positioning.

Speed issues:

• can rendering be sped up in any useful way? scrutinize output of tree code.

Set union and intersection

I really appreciate this resource. A request: given that you have set types and membership as a term constructor, could you add set intersection and union as term constructors too? I have no idea how hard that would be, but ideally you'd also have reductions so that e.g. {x, y} U {z} would reduce to {x, y, z}.

Better support for multiword expressions

We often want to be able to write something like the following in a %%lamb block (Lucas Champollion):

||a sandwich|| = Lx_e: sandwich(x)
||a_sandwich|| = Lx_e: sandwich(x)

That the second doesn't work is just a bug, underscore is being parsed wrong. The first should probably try to find a usable variable name based on the item name.

Secondary issue: Item.name isn't settable.