Skip to content

Conversation

@fblanqui
Copy link
Contributor

@fblanqui fblanqui commented Jan 16, 2023

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:

  • we only test "hol.ml"
  • we sometimes need to install the following packages: libipc-system-simple-perl, libstring-shellquote-perl
  • github accepts up to 256 jobs maximum

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

@fblanqui fblanqui closed this Jan 16, 2023
@fblanqui fblanqui changed the title add ci Add continuous integration script Jan 16, 2023
@fblanqui fblanqui reopened this Jan 16, 2023
@mpu
Copy link
Contributor

mpu commented Jan 17, 2023

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.

@fblanqui fblanqui changed the title Add continuous integration script Working ocaml-camlp5 pairs Feb 15, 2023
@fblanqui fblanqui mentioned this pull request Feb 15, 2023
@aqjune
Copy link
Contributor

aqjune commented Sep 24, 2023

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
Copy link
Owner

jrh13 commented Oct 20, 2023

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
Copy link
Contributor Author

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
Copy link
Contributor

aqjune commented Oct 23, 2023

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.

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

4 participants