Here’s something we’ve been testing out; we thought some of you would like to try it.
It’s an experimental version so please account for that when using it. Any feedback is much appreciated
Answer generated by large language models, please double check for correctness. Search results provided by Mojeek. Projects on Mojeek Labs are experimental and liable to break or go down.
N.B. works in English, French, Italian, German and Spanish; will likely perform best in English currently.
I would put the Mojeek spell check up at the top like it is with regular search. I misspelled a word and Labs did okay with the text but some of the links were off.
I then intentionally did some searches with misspellings and then the correct spelling. On the misspelling the text seemed to give me an answer for the proper spelling however the text was totally different for the correct spelling.
Despite the spelling thing this is really interesting and has a lot of promise.
Also, it looks like the URL entities are being double encoded: %2520 instead of %20
# Query
where can i find information on tla+
# URL
https://labs.mojeek.com/rag/search.html?q=where%2520can%2520i%2520find%2520information%2520on%2520tla%252B&rid=kbcYRconiQeoaY4KHZlBD
# Result
Answer
TLA+ is a specification language for concurrent systems, and you can find
information about it in several places.
One resource is Ron Pressler's blog series about TLA+, which provides an
introduction and history of the language 1.
Another source is the website for TEACHLEARNACHIEVE (TLA) LTD, which provides
information about the company and its use of TLA+ 2.
You can also find information about TLA+ on GitHub, where the TLA+Toolbox and
TLC model checker are hosted 3.
Additionally, there is an article from 2014 that describes the use of TLA+ in
an industrial environment, including its benefits and limitations 4.
TLA+ was introduced in 1999 and is based on the temporal logic of actions, as
described in 5.
The TLA+ Proof System, or TLAPS, is used to mechanically check proofs written
in TLA+ 5.
There are also tools for translating algorithms written in PlusCal into TLA+
models and running them through the model checker [citation:itation:7].
TLA+ is a large and complex language, with PlusCal built on top of it, and
there is a syntax cheatsheet available to help understand the symbols used in
the language 8.
Sources
TLA+ in Practice and Theory
1 - pron.github.io
TEACHLEARNACHIEVE (TLA) LTD - Free Company Check
2 - www.companieslist.co.uk
GitHub - tlaplus/tlaplus: TLC is a model checker
3 - github.com
Industrial Use of TLA+
4 - lamport.azurewebsites.net
TLA+ - Wikipedia
5 - en.wikipedia.org
Beyond the Toolbox — Learn TLA+
6 - learntla.com
TLA+ Helps Programmers Squash Bugs Before Coding -
7 - spectrum.ieee.org
An Introduction to TLA+ and Its Use in Parties —
8 - www.innoq.com
Related
What is the first installment in Ron Pressler's blog series about TLA +?
What is the name of the Private Limited Company TEACHLEARNACHIEVE (TLA) LTD's
website?
What is the GitHub repository for TLC, the model checker for TLA+?
What is the article that provides an excellent picture of TLA+ use in an
industrial environment?
If Mojeek is using a RAG then is it possible to increase the crawl rate of weather forecasts (like news currently is) and to allow questions like: Will it rain in Chicago today? or When is the latest I can cut the grass today?
I’m not sure if that is interesting to Mojeek or if that would be too many trivial API requests like the issues with Siri and Alexa.
This is a little bit more complex than just crawl rate - better query handling and matching for example would help. It’s something that we’re definitely looking into.