BibtexQuery CI

Stream: general

[Kim Morrison]

The BibtexQuery repository is part of our essential infrastructure, as a dependency of doc-gen4.

It currently doesn't have any CI set up. Would anyone be interested in jumping in and doing this? It is probably sufficient to just use the basic lean-action Github action that lake init provides.

[Kim Morrison]

The repository belongs to @Frédéric Dupuis. Also potentially interested in doing this would be @Jz Pan, who introduced that dependency in doc-gen4.

But all welcome. :-)

[Jz Pan]

Kim Morrison said:

The BibtexQuery repository is part of our essential infrastructure, as a dependency of doc-gen4.

It currently doesn't have any CI set up. Would anyone be interested in jumping in and doing this? It is probably sufficient to just use the basic lean-action Github action that lake init provides.

I think it's a good idea. However I'm not familiar with github CI infrastructure. Maybe we can copy some CI-related code from doc-gen4, since I remembered that there is a CI workflow.

[Henrik Böving]

doc-gen's CI workflow is not using lean-action yet (though we could also change that if people want to)

[Kim Morrison]

I wouldn't copy from doc-gen. Just run lake new to get a fresh repository, then mimic the CI setup provided there. It is minimal, but all that is needed for BibtexQuery.

[François G. Dorais]

Done at BibtexQuery#15

[Frédéric Dupuis]

I just merged it, but I have no idea what this actually does. What sort of CI do we get here?

[François G. Dorais]

Now, every time there is a push or PR or manually trigger it, a test build will be run. So now you can wait for the checkmark instead of trying it on your computer, for example.

[François G. Dorais]

@Frédéric Dupuis I just created a dummy PR for you so you can see it in action.

[Jz Pan]

Is it possible to run a test after build finished? For example lake exe bibtex-query l references.bib on a fixed version of mathlib's references file, to see if it can be processed correctly.

[Kim Morrison]

Yes, definitely. Have a look at the lakefile.lean / toml's of a few projects to see how it is done. testDriver and testDriverArgs are the relevant settings.

[Kim Morrison]

You can arrange so that lake test either runs an arbitrary lake exe ...., or just compiles a separate library.

[Austin Letson]

Henrik Böving said:

doc-gen's CI workflow is not using lean-action yet (though we could also change that if people want to)

I opened a PR to use lean-action in doc-gen

[Austin Letson]

We could also potentially wrap the test_docs.sh script in a testDriver to use lake test.

[Henrik Böving]

Austin Letson said:

We could also potentially wrap the test_docs.sh script in a testDriver to use lake test.

I think it's fine to keep it this way for now.