Skip to content

Cache global metadata in separate meta.sqlite3 database#80

Merged
c-cube merged 2 commits intosneeuwballen:masterfrom
bclement-ocp:meta-cache
Mar 21, 2025
Merged

Cache global metadata in separate meta.sqlite3 database#80
c-cube merged 2 commits intosneeuwballen:masterfrom
bclement-ocp:meta-cache

Conversation

@bclement-ocp
Copy link
Contributor

This makes it faster to access the prover metadata for all runs in the compare2 view because we don't have to open a bajillion different databases (goes from several minutes to a few seconds for me when restarting the server).

Note that the database cache is not currently garbage collected and might need to be manually cleaned periodically.

This makes it faster to access the prover metadata for all runs in the
`compare2` view because we don't have to open a bajillion different
databases (goes from several minutes to a few seconds for me when
restarting the server).

Note that the database cache is not currently garbage collected and
might need to be manually cleaned periodically.
Copy link
Member

@c-cube c-cube left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Very useful! I'm not super fond of the key/value table, but it's flexible. I'm open to merging after we discuss my few questions :)

CREATE TABLE IF NOT EXISTS test_database (
id INTEGER PRIMARY KEY,
path BLOB NOT NULL UNIQUE
);
Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I think all these tables could be strict now :)

Copy link
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Interesting, did not know sqlite supported strict typing now!

key TEXT NOT NULL,
value BLOB,
CONSTRAINT meta_key_unique UNIQUE (database_id, key)
);
Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I think you're going to want to build an index on (database_id, key) for faster access.

Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

also: it could be easier, maybe, to use a JSON field (sqlite supports json). I'm not sure.

Copy link
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I believe that the UNIQUE constraint creates such an index already.

https://www.sqlite.org/lang_createtable.html#unique_constraints

Also did not know sqlite had json support, all this new stuff! It might have been easier to use json from the get-go but now that the code is written I am a bit reluctant to rewrite it if it's not necessary. It's also consistent with the way data is stored elsewhere (which I think pre-dates json support).

Copy link
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

By "elsewhere" I mean: in Test_metadata.

Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

that's fair! It's just good to know for next time :). The JSON support is very close to PG's afaik, and it's useful for flexible columns. But no need to rewrite your code.

Copy link
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Actually I was more concerned with the OCaml side of things than the SQLite side of things re: json, but now that I think about it there's already a json printer in the Misc module and it's probably just strings at the Sqlite3 level so I can actually change this quickly I think, let me have a go.

Copy link
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Actually there's no json parsing so forget it.

@c-cube c-cube merged commit b0033cb into sneeuwballen:master Mar 21, 2025
2 checks passed
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

2 participants