tjh.dev
1{
2 lib,
3 mkCoqDerivation,
4 coq,
5 mathcomp,
6 mathcomp-algebra-tactics,
7 mathcomp-word,
8 version ? null,
9}:
10
11mkCoqDerivation {
12 pname = "jasmin";
13 owner = "jasmin-lang";
14
15 inherit version;
16 defaultVersion =
17 let
18 case = coq: mc: out: {
19 cases = [
20 coq
21 mc
22 ];
23 inherit out;
24 };
25 in
26 with lib.versions;
27 lib.switch
28 [ coq.coq-version mathcomp.version ]
29 [
30 (case (range "8.19" "9.1") (range "2.2" "2.4") "2025.02.0")
31 (case (isEq "8.18") (isEq "2.2") "2024.07.2")
32 ]
33 null;
34 releaseRev = v: "v${v}";
35
36 release."2025.02.0".sha256 = "sha256-Jlf0+VPuYWXdWyKHKHSp7h/HuCCp4VkcrgDAmh7pi5s=";
37 release."2024.07.3".sha256 = "sha256-n/X8d7ILuZ07l24Ij8TxbQzAG7E8kldWFcUI65W4r+c=";
38 release."2024.07.2".sha256 = "sha256-aF8SYY5jRxQ6iEr7t6mRN3BEmIDhJ53PGhuZiJGB+i8=";
39
40 propagatedBuildInputs = [
41 mathcomp-algebra-tactics
42 mathcomp-word
43 ];
44
45 makeFlags = [
46 "-C"
47 "proofs"
48 ];
49
50 meta = with lib; {
51 description = "Jasmin language & verified compiler";
52 homepage = "https://github.com/jasmin-lang/jasmin/";
53 license = licenses.mit;
54 maintainers = with maintainers; [
55 proux01
56 vbgl
57 ];
58 };
59}