* Using ConTeXt-LMTX for modern Mathematically-Literate-Programming 2/2 @ 2020-11-30 9:51 Stephen Gaito [not found] ` <83c1393f-f11e-9260-9593-16c6f8c42189@xs4all.nl> 0 siblings, 1 reply; 4+ messages in thread From: Stephen Gaito @ 2020-11-30 9:51 UTC (permalink / raw) To: ntg-context Hello (again), This email is further to my previous "Using ConTeXt-LMTX for modern Mathematically-Literate-Programming 1/2" email... My ultimate goal in using ConTeXt-LMTX as a Mathematically-Literate-Programming tool, is to actually write a kernel "Mathematical Language" in ANSI-C (wrapped in Lua) which is then imported back into ConTeXt-LMTX as a standard Lua module (with an ANSI-C shared library). This would allow the output of "code" in my "Mathematical Language" to be directly embedded/typeset in the output of my Mathematical document. (The ultimate goal is to ensure that there is NO wishful thinking that the code is "correct" ("just trust me")... all results would be directly visible in the PDF). Alas, while, for other reasons, trying to use the Lua-CJSON Lua module from within ConTeXt-LMTX (which also makes use of a shared library written in C), I find that the current ConTeXt-LMTX is missing (among potentially others) the `lua_checkstack` symbol: > ...Xt/tex/texmf-context/tex/context/base/mkiv/l-package.lua:333: error > loading module 'cjson' from file '/usr/local/lib/lua/5.4/cjson.so': > /usr/local/lib/lua/5.4/cjson.so: undefined symbol: lua_checkstack even when using the ConTeXt/LuaMetaTeX `--permiteloadlib` switch. (Note that this Lua-CJSON module does work with the native 5.4 Lua). (The ConTeXt I am using identifies itself as: ConTeXt ver: 2020.11.25 19:18 LMTX fmt: 2020.11.25 int: english/english) I note that the output of `luametatex --help` includes the following statement: > Loading libraries is blocked unless one explicitly permits it (will > be in 2.08+): > > --permitloadlib permit loading of external libraries (coming) ---- QUESTIONS: 1. Is this an oversight and `--permitloadlib` is meant to be working now? 2. Is this a trivial fix (and might be fixed soon -- time permitting)? 3. Is this a rather complex refactoring of the code/build system (and hence might take some time before a fix can be rolled out)? 4. Is this a case of "the `lua_checkstack` symbol will never be part of luametatex"? ---- Any of the above scenarios is OK (though scenario 4 would be a disappointment as it means no shared library lua modules could be used in ConTeXt)... ... it would however be useful to have an idea of which scenario is most likely. Again Many thanks for a wonderful (and stable) tool! Regards, Stephen Gaito ___________________________________________________________________________________ If your question is of interest to others as well, please add an entry to the Wiki! maillist : ntg-context@ntg.nl / http://www.ntg.nl/mailman/listinfo/ntg-context webpage : http://www.pragma-ade.nl / http://context.aanhet.net archive : https://bitbucket.org/phg/context-mirror/commits/ wiki : http://contextgarden.net ___________________________________________________________________________________ ^ permalink raw reply [flat|nested] 4+ messages in thread
[parent not found: <83c1393f-f11e-9260-9593-16c6f8c42189@xs4all.nl>]
* Re: Using ConTeXt-LMTX for modern Mathematically-Literate-Programming 2/2 [not found] ` <83c1393f-f11e-9260-9593-16c6f8c42189@xs4all.nl> @ 2020-12-02 10:43 ` Stephen Gaito 2020-12-02 13:17 ` Hans Hagen 0 siblings, 1 reply; 4+ messages in thread From: Stephen Gaito @ 2020-12-02 10:43 UTC (permalink / raw) To: mailing list for ConTeXt users Hans, Many thanks for your comments... see below. On Mon, 30 Nov 2020 19:31:55 +0100 Hans Hagen <j.hagen@xs4all.nl> wrote: > On 11/30/2020 10:51 AM, Stephen Gaito wrote: > > Hello (again), > > > > This email is further to my previous "Using ConTeXt-LMTX for modern > > Mathematically-Literate-Programming 1/2" email... > > > > My ultimate goal in using ConTeXt-LMTX as a > > Mathematically-Literate-Programming tool, is to actually write a > > kernel "Mathematical Language" in ANSI-C (wrapped in Lua) which is > > then imported back into ConTeXt-LMTX as a standard Lua module (with > > an ANSI-C shared library). > > Just curious: do you think that using c instead of lua for that has > advantages? This is a very good and important question. One I have asked myself repeatedly. My ultimate goal is to write a small mathematical kernel in ANSI-C, which is, using [Frama-C](https://frama-c.com/), proven *correct*. To my knowledge, Lua has no similar tool for correctness proofs. Equally importantly, there are a very wide range of very different compilers which compile ANSI-C for an equally very wide range of CPU's. Again, to my knowledge, Lua v5.4 has only one implementation (though this implementation *can* be compiled for a very wide range of CPU's). The problem here is that Mathematicians are inherently very conservative about the concept of "proof" (it has taken well over 2,000 hard years to develop our current understanding). My kernel will be an extensible "proof" engine. For mathematicians to trust it, this proof engine must itself be proven correct (or as correct as currently possible). It must also be simple enough to *see* that it is correct (hence the Literate-Programming approach), *and* (since I can not even hope to prove the compilers are *correct*), there must be many *different* compiler implementations (to show that the results are not artefacts of one particular implementation). Finally, the computational complexity of my proof engine, will be comparable to MetaFun/MetaPost... which I suspect you would not consider implementing in pure Lua. Some things are faster in C. So yes I do need to implement it in ANSI-C wrapped in Lua (so that it can be used from *inside* ConTeXt). Since this is a mathematical tool, "embedding" it in ConTeXt is ideal. As a mathematician writes, what they write gets proof-checked automatically... in the document they are writing, and by the typesetting tool they are using for the finished PDF. :-) ConTeXt (via LuaMetaTex) makes this possible in a way native TeX/LaTeX never could. So once again, many many thanks for the vision to create such a flexible tool! > > > This would allow the output of "code" in my "Mathematical Language" > > to be directly embedded/typeset in the output of my Mathematical > > document. > > > > (The ultimate goal is to ensure that there is NO wishful thinking > > that the code is "correct" ("just trust me")... all results would be > > directly visible in the PDF). > > > > Alas, while, for other reasons, trying to use the Lua-CJSON Lua > > module from within ConTeXt-LMTX (which also makes use of a shared > > library written in C), I find that the current ConTeXt-LMTX is > > missing (among potentially others) the `lua_checkstack` symbol: > > could be .. we dont' use it > > >> ...Xt/tex/texmf-context/tex/context/base/mkiv/l-package.lua:333: > >> error loading module 'cjson' from file > >> '/usr/local/lib/lua/5.4/cjson.so': > >> /usr/local/lib/lua/5.4/cjson.so: undefined symbol: lua_checkstack > > > > even when using the ConTeXt/LuaMetaTeX `--permiteloadlib` switch. > > > > (Note that this Lua-CJSON module does work with the native 5.4 Lua). > > why not use the build in helpers The test, which triggered the error message (above), was to prove that I could send [NATS](https://nats.io/) messages from *inside* ConTeXt. "Out of the box", the [Lua-NATS](https://github.com/DawnAngel/lua-nats) requires: - luasocket (which LuaMetaTex provides, many many thanks!) - lua-cjson (which is an external shared library and is what I was testing) Fortunately, I found a couple of pure Lua JSON tools which I could get Lua-NATS to use with a one line change. (And, for the record, I *can* send and receive messages from a NATS server from inside ConTeXt :-) If I find I need to make changes to the Lua-NATS code, I will probably use LuaMetaTeX's internal JSON implementation as you suggest below (again many thanks for embedding a JSON implementation). Using Lua-NATS is part of my larger goal to parallelize the typesetting of large documents using ConTeXt (more on this in another email). > > \usemodule[json] > > \starttext > > \startluacode > local l = { a = 1, b = { c = "d" } } > inspect(l) > local j = utilities.json.tojson(l) > inspect(j) > local s = utilities.json.tostring(j) > inspect(s) > io.savedata("temp.json",j) > local t = utilities.json.load("temp.json") > inspect(t) > \stopluacode > > \stoptext > > > 1. Is this an oversight and `--permitloadlib` is meant to be working > > now? > > I dont' know. I never use external modules myself (in luatex I use(d) > ffi for some database acces but those (and a few more) are build in > luametatex as optional modules (as minimalistic as possible lua > itself can do most). I don't want a bloated bianry with all kind of > dependencies that force constant updates. A very important consideration. > > > 2. Is this a trivial fix (and might be fixed soon -- time > > permitting)? > > It's probably a side effect of binaries being stripped cq. functions > being inlined and we don't use lua_checkstack in luametatex. We can > at some point probably add some 'don't strip' feature (which then of > course exposes a whole bunch more that then for sure gets abused and > triggers issues when they change) > > > 3. Is this a rather complex refactoring of the code/build system > > (and hence might take some time before a fix can be rolled > > out)? > > dunno, a such things are driven by demand (and when it doesn't fit > into the 'fun to do' it has to be part of some project) > > > 4. Is this a case of "the `lua_checkstack` symbol will never be > > part of luametatex"? > > dunno, i haven't figured out how to selectively strip and making lua > into a lib that is loaded at runtime adds a dependency and > installation hassle (apart from the fact that when users then kick in > their own variant we need to support it which agsin is not that much > fun) > > > Any of the above scenarios is OK (though scenario 4 would be a > > disappointment as it means no shared library lua modules could be > > used in ConTeXt)... > > at some point (when we're stable and mojca and i have some more > infractstucrure set up, we have some ideas but are not in a hurry) > the source of luatex will be in the distribution and then users can > add their own optional modules If you ever want/need a beta tester of writing and building these optional modules, please let me know. For the moment, I suspect I will "simply" use Lua-NATS to request the proof-computations from an external Docker/Podman container process. Given the size and complexity of the proof-computations, the required network traffic will probably be nearly insignificant. > > > ... it would however be useful to have an idea of which scenario is > > most likely. > > As I said before, again many thanks for a wonderful (and stable) tool! Regards, Stephen Gaito > ----------------------------------------------------------------- > Hans Hagen | PRAGMA ADE > Ridderstraat 27 | 8061 GH Hasselt | The Netherlands > tel: 038 477 53 69 | www.pragma-ade.nl | www.pragma-pod.nl > ----------------------------------------------------------------- ___________________________________________________________________________________ If your question is of interest to others as well, please add an entry to the Wiki! maillist : ntg-context@ntg.nl / http://www.ntg.nl/mailman/listinfo/ntg-context webpage : http://www.pragma-ade.nl / http://context.aanhet.net archive : https://bitbucket.org/phg/context-mirror/commits/ wiki : http://contextgarden.net ___________________________________________________________________________________ ^ permalink raw reply [flat|nested] 4+ messages in thread
* Re: Using ConTeXt-LMTX for modern Mathematically-Literate-Programming 2/2 2020-12-02 10:43 ` Stephen Gaito @ 2020-12-02 13:17 ` Hans Hagen 2020-12-03 10:43 ` Stephen Gaito 0 siblings, 1 reply; 4+ messages in thread From: Hans Hagen @ 2020-12-02 13:17 UTC (permalink / raw) To: mailing list for ConTeXt users, Stephen Gaito On 12/2/2020 11:43 AM, Stephen Gaito wrote: > Again, to my knowledge, Lua v5.4 has only one implementation (though > this implementation *can* be compiled for a very wide range of CPU's). Lua has not many demands ... it can even run on tiny cpu's. It's all rather plain C code. (And in luametatex we have no c++ ... all is just C.) > Finally, the computational complexity of my proof engine, will be > comparable to MetaFun/MetaPost... which I suspect you would not > consider implementing in pure Lua. Some things are faster in C. Hard to say ... I think that the parser / expansion machinery in mp is the bottleneck here (no fun to do that in lua). Redoing it in Lua also is asking for compatibility issues. (btw, extensions are done in lua anyway, as is the mp backend) > So yes I do need to implement it in ANSI-C wrapped in Lua (so that it > can be used from *inside* ConTeXt). I would have to see the 'kind of code involved' in order to comment on that. An option is to do most in lua and maybe some helpers for crititical code in C. Hans ----------------------------------------------------------------- Hans Hagen | PRAGMA ADE Ridderstraat 27 | 8061 GH Hasselt | The Netherlands tel: 038 477 53 69 | www.pragma-ade.nl | www.pragma-pod.nl ----------------------------------------------------------------- ___________________________________________________________________________________ If your question is of interest to others as well, please add an entry to the Wiki! maillist : ntg-context@ntg.nl / http://www.ntg.nl/mailman/listinfo/ntg-context webpage : http://www.pragma-ade.nl / http://context.aanhet.net archive : https://bitbucket.org/phg/context-mirror/commits/ wiki : http://contextgarden.net ___________________________________________________________________________________ ^ permalink raw reply [flat|nested] 4+ messages in thread
* Re: Using ConTeXt-LMTX for modern Mathematically-Literate-Programming 2/2 2020-12-02 13:17 ` Hans Hagen @ 2020-12-03 10:43 ` Stephen Gaito 0 siblings, 0 replies; 4+ messages in thread From: Stephen Gaito @ 2020-12-03 10:43 UTC (permalink / raw) Cc: mailing list for ConTeXt users Hans, If my only constraints were ease of programming and moderate performance, I would completely agree that using mostly Lua plus (possibly) some C code for some targeted stuff that is really slow in Lua is the correct solution.... we are actually in agreement. Unfortunately, I have the *non-functional* requirement to *prove* the code's correctness.... this is the heart of what I have to write about. There is no getting out of this requirement.... So, some day it would be very useful to be able to directly embed a Lua wrapped ANSI-C shared library inside the new LuaMetaTex.... However, at the moment, as part of my parallelization attempts I can interact with my ANSI-C code over a network.... so I will use this approach for the near to medium time frames. Regards, Stephen Gaito On Wed, 2 Dec 2020 14:17:54 +0100 Hans Hagen <j.hagen@xs4all.nl> wrote: > On 12/2/2020 11:43 AM, Stephen Gaito wrote: > > > Again, to my knowledge, Lua v5.4 has only one implementation (though > > this implementation *can* be compiled for a very wide range of > > CPU's). > > Lua has not many demands ... it can even run on tiny cpu's. It's all > rather plain C code. (And in luametatex we have no c++ ... all is > just C.) > > > Finally, the computational complexity of my proof engine, will be > > comparable to MetaFun/MetaPost... which I suspect you would not > > consider implementing in pure Lua. Some things are faster in C. > > Hard to say ... I think that the parser / expansion machinery in mp > is the bottleneck here (no fun to do that in lua). Redoing it in Lua > also is asking for compatibility issues. (btw, extensions are done in > lua anyway, as is the mp backend) > > > So yes I do need to implement it in ANSI-C wrapped in Lua (so that > > it can be used from *inside* ConTeXt). > > I would have to see the 'kind of code involved' in order to comment > on that. > > An option is to do most in lua and maybe some helpers for crititical > code in C. > Hans > > > ----------------------------------------------------------------- > Hans Hagen | PRAGMA ADE > Ridderstraat 27 | 8061 GH Hasselt | The Netherlands > tel: 038 477 53 69 | www.pragma-ade.nl | www.pragma-pod.nl > ----------------------------------------------------------------- ___________________________________________________________________________________ If your question is of interest to others as well, please add an entry to the Wiki! maillist : ntg-context@ntg.nl / http://www.ntg.nl/mailman/listinfo/ntg-context webpage : http://www.pragma-ade.nl / http://context.aanhet.net archive : https://bitbucket.org/phg/context-mirror/commits/ wiki : http://contextgarden.net ___________________________________________________________________________________ ^ permalink raw reply [flat|nested] 4+ messages in thread
end of thread, other threads:[~2020-12-03 10:43 UTC | newest] Thread overview: 4+ messages (download: mbox.gz / follow: Atom feed) -- links below jump to the message on this page -- 2020-11-30 9:51 Using ConTeXt-LMTX for modern Mathematically-Literate-Programming 2/2 Stephen Gaito [not found] ` <83c1393f-f11e-9260-9593-16c6f8c42189@xs4all.nl> 2020-12-02 10:43 ` Stephen Gaito 2020-12-02 13:17 ` Hans Hagen 2020-12-03 10:43 ` Stephen Gaito
This is a public inbox, see mirroring instructions for how to clone and mirror all data and code used for this inbox; as well as URLs for NNTP newsgroup(s).