Skip to content

Custom location of the websearch database #1230

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Open
Alidra opened this issue Apr 2, 2025 · 0 comments · May be fixed by #1235
Open

Custom location of the websearch database #1230

Alidra opened this issue Apr 2, 2025 · 0 comments · May be fixed by #1235

Comments

@Alidra
Copy link
Member

Alidra commented Apr 2, 2025

It should be possible to customize the location of the websearch database (currently it must in a ~/.LPSearch.db file).
This can be useful if one wants to start different servers indexing different libraries or to allow collaborative management of a server in work (for instance the one referencing the HOL-Light library) without having to use different ~/.LPSearch.db files (one for each user launching the server).

Note that an alternative solution would be to generate the ~/.LPSearch.db file then move it to a custom folder and start the webserver from that location.
Then, Lambdapi should look for it in the current folder since it fails to find it in the HOME folder of the user. This solution is however not very elegant.

@Alidra Alidra self-assigned this Apr 2, 2025
@Alidra Alidra linked a pull request Apr 10, 2025 that will close this issue
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Projects
None yet
Development

Successfully merging a pull request may close this issue.

1 participant