jrh13 / hol-light

The HOL Light theorem prover
Other
435 stars 79 forks source link

Working ocaml-camlp5 pairs #71

Open fblanqui opened 1 year ago

fblanqui commented 1 year ago

Please do not merge this PR but keep it open: its purpose is to provide data on working ocaml-camlp5 pairs.

It contains some github action scripts to inventory the pairs ocaml-camlp5 for which hol-light works.

For each camlp5 version, there is a yml script testing the ocaml versions meaningful for this camlp5 version.

Remarks:

Working pairs found (this may not be exhaustive):

ocaml camlp5
4.02.3 6.14, 6.15, 6.16, 6.17, 7.01, 7.03, 7.05, 7.06.10-g84ce6cc4, 7.08, 7.1
4.03.0 6.15, 6.16, 6.17, 7.01, 7.03, 7.05, 7.06.10-g84ce6cc4, 7.08, 7.1
4.04.2 7.01, 7.03, 7.05, 7.06.10-g84ce6cc4, 7.08, 7.1
4.05.0 7.01, 7.03, 7.05, 7.06.10-g84ce6cc4, 7.08, 7.1
4.06.1 7.05, 7.06.10-g84ce6cc4, 7.08, 7.11, 7.12, 7.13, 7.14
4.07.1 7.06.10-g84ce6cc4, 7.08, 7.11, 7.12, 7.13, 7.14
4.08.1 7.09, 7.11, 7.12, 7.13, 7.14, 8.00.03, 8.00.04
4.09.1 7.11, 7.12, 7.13, 7.14, 8.00.03, 8.00.04
4.10.2 7.14, 8.00.03, 8.00.04, 8.00.05, 8.02.00, 8.02.01
4.11.2 7.14, 8.00.03, 8.00.04, 8.00.05, 8.02.00, 8.02.01
4.12.1 7.14, 8.00.03, 8.00.04, 8.00.05, 8.02.00, 8.02.01
4.13.1 8.00.03, 8.00.04, 8.00.05, 8.02.00, 8.02.01
4.14.1 8.00.03, 8.00.04, 8.00.05, 8.02.00, 8.02.01
5.0.0 8.02.01
5.1.1 8.02.01

Detailed results can be found in:

camlp5 results
8.02.01 https://github.com/fblanqui/hol-light/actions/runs/8710772959
8.02.00 https://github.com/fblanqui/hol-light/actions/runs/6954163355
8.01.00 https://github.com/fblanqui/hol-light/actions/runs/6954163352
8.00.05 https://github.com/fblanqui/hol-light/actions/runs/4185147934
8.00.04 https://github.com/fblanqui/hol-light/actions/runs/4127325386
8.00.03 https://github.com/fblanqui/hol-light/actions/runs/4127325387
8.00.02 https://github.com/fblanqui/hol-light/actions/runs/4127325397
other https://github.com/fblanqui/hol-light/actions/runs/3929583606
mpu commented 1 year ago

Would it be possible to run holtest instead of simply loading the prelude? That may be too resource-consuming, so maybe a lighter version of holtest can be adapted.

aqjune commented 1 year ago

Hi, I have a question about CI. Are they running on a custom server, or Github-hosted server? If the answer is latter, how is it related to the monetary cost for Github CI?

jrh13 commented 1 year ago

I really like the principle, but am a bit nervous about the resource usage running it in CI. Currently the hol-light repo only uses whatever is provided in a free Github account. Do you think this is a needless concern?

fblanqui commented 1 year ago

Hi John. Actually, this PR does not need to be merged: you can just leave it open. I added a comment at the beginning of the PR description about this. CI is launched only if it is updated, which can be done from time to time only.

aqjune commented 1 year ago

For its even lighter version I made a pull request here: #85 :) This pull request (#71) will still be valuable because it tracks all valid configurations of ocaml and camlp5.