leanprover-community / lean4game

Server to host lean games.
https://adam.math.hhu.de
GNU General Public License v3.0
197 stars 35 forks source link

Adding Image to the left side pane of a world #235

Open JadAbouHawili opened 5 months ago

JadAbouHawili commented 5 months ago

Using the Image command from the docs, the image will appear in the middle. Is there a way to make the image appear on the left pane, or that's not supported?

joneugster commented 5 months ago

Not supported right now. What would be the use case? Why would you prefer to have the image there?

And do you mean as background of the chat (being covered by the blue chat messages) or would you like to add an image as one of the chat messages?

JadAbouHawili commented 5 months ago

I was making a Logic world and wanted to include a picture of a truth table in the left side pane before entering the first level, I know you could do it in ascii but thought the picture would look nicer. Truth-Table-And

JadAbouHawili commented 5 months ago

Would also be nice to do for levels, and I guess that would target the same command which is Introduction

joneugster commented 5 months ago

I cant test this until Monday, but all images in the images/ folder are publicly exposed, like this: https://adam.math.hhu.de/data/g/hhu-adam/robo/images/Robo.png

So I wonder if putting somehing like <img src="data/g/hhu-adam/robo/images/Robo.png" /> into the Introduction or Hint would work.

(even if it did, that would be a feature that can easily be improved and documented👍)

JadAbouHawili commented 5 months ago

What I have tested: (in introduction of a level) \<img src='images/Logic/Truth-Table-And.png' /> \<img src='data/g/hhu-adam/robo/images/Robo.png' /> Both display as text.

joneugster commented 5 months ago

At least partially fixed on dev: <img src=\"https://url.com/to/image\"/> will work.

Ideally one could embed images from the local images/ folder directly (so that it also works in local setups), but rn I don't know how to do that, besides what's now in the manual.

JadAbouHawili commented 4 months ago

I was able to write the following latex which can be used as a truthtable instead of an image or ascii:

$
\\begin{array}{|c c|c|} 
a & b & F \\\\
\\hline
0 & 0 & 0 \\\\
0 & 1 & 0 \\\\
1 & 0 & 0 \\\\
1 & 1 & 1 
\\end{array}
$

Are you open to adding more examples about latex usage? If so, I think things like this would be a useful addition and I'm willing to work on more examples. I decided to do this because the ascii looks lame in comparision

TentativeConvert commented 4 months ago

Yes, I think it would be good to include some examples of latex usage in the documentation. I'm surprised, however, that the above example works. My experience was that I need to escape {…} as \{…}, e.g.:

 $$
  A_\{i,j} \\cdot 
  \\begin\{pmatrix}
  0 & 0 & 0\\\\
  1 & 0 & 0 \\\\
  0 & 0 & 0 
  \\end\{pmatrix}
  =
  \\begin\{pmatrix}
  0 & 0 & 0\\\\
  A_\{i,j} & 0 & 0 \\\\
  0 & 0 & 0 
  \\end\{pmatrix}
  $$

(see this file) Maybe it depends on the context?

joneugster commented 4 months ago

You need to escape { as \{ in Hints only, but not the introducrion/conclusion/statement doc string.

As for documentation, this section is a start but could be improved.

joneugster commented 4 months ago

I would love PRs extending/improving the doc!

(The issues about images will be resolved independently and will follow too)