search

leanprover-community / mathport

Mathport is a tool for porting Lean3 projects to Lean4
Apache License 2.0
41 stars 15 forks source link

chore: run every 12 hours #208

Closed semorrison closed 1 year ago

semorrison commented 1 year ago

Per request on zulip.

gebner commented 1 year ago

You also need to change the predata.yml file.

We currently have two jobs: predata & build. Predata compiles mathlib and produces .ast.json and .tlean files. And then build runs mathport on them. They are very loosely coupled btw (build is scheduled a couple hours after predata and takes the latest predata release).