Express.js Updated 2025-02-22 +Created 1970-01-01
View more
This doesn't do a hole lot. Ciro Santilli wouldn't really call it a web framework. It's more like a middleware. Real web frameworks are built on top of it.
Examples under: nodejs/express:
  • nodejs/express/min.js: minimal example. Visit localhost:3000 and it shows hello world. It is a bit wrong because the headers say HTML but we return plaintext.
  • nodejs/express/index.js: example dump with automated tests where possible. The automated tests are run at startup after the server launches. Then the server keeps running so you can interact with it.
A live example on Heroku can be seen at: github.com/cirosantilli/heroku-node-min
Read the full article
FeathersJS Updated 2025-02-22 +Created 1970-01-01
View more
Looks interesting.
It seems to abstract the part about the client messaging the backend, which focuses on being able to easily plug in a number of Front-end web framework to manage client state.
Has the "main web API is the same as the REST API" focus, which is fundamental 2020-nowadays.
Uses Socket.IO, which allows the client Javascript to register callbacks when data is updated to achieve Socket.IO, e.g. their default chat app does:
client.service('messages').on('created', addMessage);
so that message appear immediately as they are sent.
Their standard template from feathers generate app on @feathersjs/cli@4.5.0 includes:
  • several authentication methods, including OAuth
  • testing
  • backend database with one of several object-relational mapping! However, they don't abstract across them. E.g., the default Chat example uses NeDB, but a real app will likely use Sequelize, and a port is needed
which looks promising! They don't have a default template for a Front-end web framework however unfortunately: docs.feathersjs.com/guides/frameworks.html#the-feathers-chat lists a few chat app versions, which is their hello world:
But it is in itself a completely boring app with a single splash page, and no database interaction, so not a good showcase. The actual showcase app is feathersjs/feathers-chat.
And there is no official example of the chat app that is immediately deployable to Heroku: FeathersJS Heroku deployment, all setups require thinking.
Global source entry point: determine on package.json as usual, defaults to src/index.js.
Read the full article
feathersjs/feathers-chat Updated 2025-02-22 +Created 1970-01-01
View more
The main FeathersJS hello world demo. Notable missing things...
Read the full article
shakacode/react_on_rails Updated 2025-02-22 +Created 1970-01-01
View more
Uses Redux, while reactjs/react-rails appears to do that more manually
Live instance: www.reactrails.com/ with source at: github.com/shakacode/react-webpack-rails-tutorial Not the most advanced web-app (a gothinkster/realworld-level would be ideal). Also has clear dependency description, which is nice.
Oh, and the guy behind that project lives in Hawaii (Ciro Santilli's ideal city to live in), has an Asian-mixed son, and two Kinesis Advantage 2 keyboards as seen at twitter.com/railsonmaui/status/1377515748910755851, Ciro Santilli was jealous of him.
Read the full article
cirosantilli.com content uploaded to ourbigbook.com/cirosantilli Updated 2025-02-22 +Created 1970-01-01
View more
Managed to upload the content from the static website cirosantilli.com (OurBigBook Markup source at github.com/cirosantilli/cirosantilli.github.io) to ourbigbook.com/cirosantilli.
Although most of the key requirements were already in place since the last update, as usual doing things with the complex reference content stresses the system further and leads to the exposition of several new bugs.
The upload of OurBigBook Markup files to ourbigbook.com was done with the newly added OurBigBook CLI ourbigbook --web option. Although fully exposed to end users, the setup is not super efficient: a trully decent implementation should only upload changed files, and would basically mean reimplementing/using Git, since version diffing is what Git shines at. But I've decided not to put much emphasis on CLI upload for now, since it is expected that initially the majority of users will use the Web UI only. The functionality was added primarily to upload the reference content.
This is a major milestone, as the new content can start attracting new users, and makes the purpose of the website much clearer. Just having this more realistic content also immediately highlighted what the next development steps need to be.
Once v1.0 is reached, I will actually make all internal links of cirosantilli.com to point to ourbigbook.com/cirosantilli to try and drive some more traffic.
The new content blows up by far the limit of the free Heroku PostgreSQL database of 10k lines. This meant that I needed to upgrade the Heroku Postgres plugin from the free Hobby Dev to the 9 USD/month Hobby Basic: elements.heroku.com/addons/heroku-postgresql, so now hosting costs will increase from 7 USD/month for the dyno to 7 + 9 = 16 UDS/month. After this upgrade and uploading all of cirosantilli.com to ourbigbook.com, Heroku dashboard reads reads:
  • 30,918 rows out of 10,000,000
  • 61.0 MB (out of 10 GB)
so clearly if we are ever forced to upgrade plans again, it means that a bunch of people are using the website and that things are going very very well! Happy how this storage cost turned out so far.
One key limitation found was that Heroku RAM memory is quite limited at 512MB, and JavaScript is not exactly the most memory economical language out there. Started investigation at: github.com/ourbigbook/ourbigbook/issues/230 Initially working around that by simply splitting the largest files. We were just on the verge of what could be ran however luckily, so a few dozen splits was enough, it managed to handle 70 kB OurBigBook Markup inputs. So hopefully if we manage to optimize a bit more we will be able to set a maximum size of 100 kB and still have a good safety margin.
Read the full article
The Math Genome Project Updated 2025-02-22 +Created 1970-01-01
View more
The website was dead as of February 2025. Last archive: web.archive.org/web/20240418004442/http://www.themathgenome.com/ Pings:
They were seeking help on May 2024:
so its likely the followup death. LinkedIn post gives basic stack: MERN stack, Heroku, Supabase/MongoDB Atlas.
Appears to support multiple proof assistant backends including Lean, Hol and Coq.
A discussion on the Lean Zulip: leanprover.zulipchat.com/#narrow/stream/113488-general/topic/The.20Math.20Genome.20Project/near/352639129. Lean people are not convinced about the model in general it seems however.
TODO not viewable without login?
Has conjectures feature.
Built by this dude John Mercer:
He must be independently wealthy or something to do such a project? What a hero. But he seems to have jobs. On the side? Hardcore.
Ciro Santilli asked: discord.com/channels/1096393420408360989/1096393420408360996/1137047842159079474
Does the website actually automatically check the formal proofs, or is this intended to be implemented at some point? And if yes, is it intended to allow proofs to depend on other proofs of the website (possibly by other people)
Owner:
Hi Ciro, yes we will be releasing in-browser proof assistant environments/checkers (e.g. Lean). Our goal is not to replace the underlying open-source repos (e.g. Mathlib) so the main dependency will be on the current repos; then when statement formalizations and proofs come in and are certified they can be PR'd to the respective repos. So we will be the source of truth for the informal latex code but only a stepping stone and orchestration layer on the way to the respective formal libraries.
So apparently there will be proof checking, but nodependencies between proofs, you still have to pull request everywhing back and face the pain.
Read the full article