Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Check sail-arm and sail-riscv in CI, use matrix instead of separate files #104

Open
wants to merge 1 commit into
base: sail2
Choose a base branch
from

Conversation

Trolldemorted
Copy link
Contributor

Fixes #103

@Alasdair
Copy link
Collaborator

Alasdair commented Oct 1, 2020

I think the line:

        run: git clone https://github.com/rems-project/sail-riscv.git && eval $(opam env) && make

is missing a cd into the sail-riscv directory - I'm not sure it'll work without HOL4 and Isabelle. We had an internal Jenkins server that did this kind of matrix style CI between everything but it's become a bit awkward to use as we are now working from home and it's not public.

@Trolldemorted
Copy link
Contributor Author

I think the line:
run: git clone https://github.com/rems-project/sail-riscv.git && eval $(opam env) && make
is missing a cd into the sail-riscv directory

You are totally right, I have amended my commit

I'm not sure it'll work without HOL4 and Isabelle.

The build fails indeed, but I can't tell whether that's because of missing/broken installations of HOL4/Isabelle or something different. The build fails with this message:

sed -i 's/datatype ast/datatype (plugins only: size) ast/' generated_definitions/isabelle/RV64/Riscv_types.thy
sed: 1: "generated_definitions/i ...": extra characters at the end of g command
make: *** [generated_definitions/isabelle/RV64/Riscv.thy] Error 1
make: *** Deleting file `generated_definitions/isabelle/RV64/Riscv.thy'

Can this be related to HOL4 or Isabelle? Are you able to build the riscv models in your enviroment with the current sail2 branch?

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.

CI does not verify the models can still be compiled
2 participants