sifive / Kami

Kami - a DSL for designing Hardware in Coq, and the associated semantics and theorems for proving its correctness. Kami is inspired by Bluespec. It is actually a complete rewrite of an older version from MIT
Apache License 2.0
197 stars 11 forks source link

Add Github Actions build #116

Closed gliptak closed 4 years ago

gliptak commented 4 years ago

Signed-off-by: Gábor Lipták gliptak@gmail.com

https://github.com/gliptak/Kami/runs/543411846

COQC Tutorial/TacticsEx.v
File "./Tutorial/TacticsEx.v", line 46, characters 2-641:
Warning:
counterImpl cannot be defined because it is informative and
Incrementer_invariant is not. [cannot-define-projection,records]
File "./Tutorial/TacticsEx.v", line 46, characters 2-641:
Warning:
isSending cannot be defined because it is informative and
Incrementer_invariant is not. [cannot-define-projection,records]
File "./Tutorial/TacticsEx.v", line 46, characters 2-641:
Warning:
implEq cannot be defined because the projections counterImpl, isSending were
not defined. [cannot-define-projection,records]
File "./Tutorial/TacticsEx.v", line 46, characters 2-641:
Warning:
specEq cannot be defined because the projections isSending, counterImpl,
counterImpl were not defined. [cannot-define-projection,records]
gliptak commented 4 years ago

@sifive please review

vmurali commented 4 years ago

Our main repository that we use for CI testing is https://github.com/sifive/RiscvSpecFormal. Unfortunately, running this requires a lot of processing power and memory. We are looking at ways to reduce the footprint. I don't think we need a CI for Kami alone, as even if it compiles, there's no guarantee of it working correctly unless RiscvSpecFormal works.

gliptak commented 4 years ago

@vmurali thank you for the pointer