findfacts

Project to make Isabelle and the AFP easily searchable. Structured in:

• common: common modules
• search: search application, with core module (search-core), web application (search-webapp), and frontend ui (search-webapp-ui).
• importer: importer pipeline to import Isabelle dump into search index

Usage

• Requirements: java 15
• Build: ./sbt -Dprofiles=ui,loader clean compile test it:test
• Preparation: Initialize git submodules (git submodule init && git submodule update)

Synonyms tool

./sbt "project symbol-synonyms-tool" "run <OPTIONS>"

Example invocation:

./sbt "project symbol-synonyms-tool" "run -o common-dt/src/main/resources/solr/conf/synonyms.txt isabelle/etc/symbols"

Importer tool

Generally:

isabelle build_importer -?

Example invocation (using isabelle):

isabelle build_importer -C theorydata-0.5.0 -d '$AFP' -r localhost:8983 -i 2022_Isabelle2022_AFP2022 -a

Search webapp

Run:

./sbt "project search-webapp" run

For deployment, see the deployment repo.

Code style

This project uses the databricks style guide with some changes:

• column width: use 120.
• implicits: Only avoid them outside of well-known patterns, such as type-classes, implicit context, and pimp-my-library.
• monadic chaining: Use for-comprehensions to easily chain monads in an understandable and readable way.
• multiple parameter lists: Use multiple parameter list for partially applicable functions or to improve type inference.

Formatting is automated via scalafmt.

The importer-isabelle submodule instead adheres to the Isabelle code style.