error loading library, libleanmd4c.so

Stream: general

[Eric Wieser]

While hacking around with Verso, I've found myself wanting a custom component to render markdown. However, when I try to use https://github.com/david-christiansen/md4lean (via VersoManual.Markdown), vscode complains that it cannot load the .so file. lake build from the command line works with out issues.

[Shreyas Srinivas]

Same here on gitpod

[Shreyas Srinivas]

I opened the lean reference manual for context

[Shreyas Srinivas]

Would it be a bad idea to link the library statically or have it compiled from source from inside lake? It doesn't look too big: https://github.com/david-christiansen/md4lean/tree/main/md4c

[Eric Wieser]

I think https://github.com/acmepjz/md4lean/pull/3 fixes the md4lean issue, though of course @David Thrane Christiansen will have to sync this into their fork

[Eric Wieser]

Thanks @Jz Pan, I've made the upstream PR at https://github.com/david-christiansen/md4lean/pull/2

[David Thrane Christiansen]

Thanks! I'm on vacation until 3 Jan, but I'll look then. I should also get around to upstreaming my md4lean changes, now that I'm fairly confident in them and have used them for a bit.