Skip to content

capDL-tool: add --json mode - #90

Merged
lsf37 merged 1 commit into
seL4:masterfrom
nspin:pr/print-json
Jul 19, 2026
Merged

capDL-tool: add --json mode#90
lsf37 merged 1 commit into
seL4:masterfrom
nspin:pr/print-json

Conversation

@nspin

@nspin nspin commented Mar 25, 2026

Copy link
Copy Markdown
Member

Adds parse-capDL ... --json=spec.json ... which outputs the CapDL spec in a JSON format for use with the Rust CapDL initializer.

The Spec Haskell type here must be kept in sync with the Spec Rust type in that repository.

@nspin
nspin force-pushed the pr/print-json branch 3 times, most recently from 6187580 to 6cfa62a Compare July 7, 2026 08:11
@lsf37 lsf37 self-assigned this Jul 13, 2026
@lsf37 lsf37 added the Haskell Haskell part of capDL label Jul 13, 2026

@lsf37 lsf37 left a comment

Copy link
Copy Markdown
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

This looks good from my side, sorry it took so long to get to a review. @nspin can you please add a commit message to pacify gitlint?

@corlewis if you could also have a brief look over this, that would be great.

Eventually I'd like to add tests for this and also an automated cross-check if files produced by this tool can be read properly by the Rust side. But that can be in separate PRs.

@corlewis corlewis left a comment

Copy link
Copy Markdown
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

This looks good to me as well!

I did however struggle to follow some of the logic on a first read through, particularly in the very large where clause of translate. I have the feeling that this would be easier to read and more maintainable if most of those helpers were separated out into their own functions with type annotations, but this almost definitely isn't worth doing now.

I was also going to say something about the style in this file not matching the rest of the repository, but after a quick look online I think it's more consistent with modern Haskell style. Again, not worth doing but if anyone ever has the time it could be nice to update the old files.

Comment on lines +411 to +414
irqs =
[ (irq, translateId obj)
| (irq, obj) <- M.toAscList irqNode
]

Copy link
Copy Markdown
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Is this really the correct style for multiline list comprehensions? This specific case could probably be a single line, but if it does have to be multiple lines then I would have expected that all of it is contained inside of the list brackets.

Suggested change
irqs =
[ (irq, translateId obj)
| (irq, obj) <- M.toAscList irqNode
]
[ (irq, translateId obj)
| (irq, obj) <- M.toAscList irqNode
]

Copy link
Copy Markdown
Member Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I'm having trouble finding an authoritative source that clearly states the convention here, but as far as I am aware, the current indentation follows a prevailing convention.

Comment thread capDL-tool/CapDL/PrintJSON.hs Outdated
Comment thread capDL-tool/CapDL/PrintJSON.hs
@corlewis

Copy link
Copy Markdown
Member

Eventually I'd like to add tests for this and also an automated cross-check if files produced by this tool can be read properly by the Rust side. But that can be in separate PRs.

Were you thinking of something more complicated, or just basic processing tests like we do with the examples in this repository? Something like that for this format would be nice, to at least make sure that other changes to the tool don't break things in unexpected ways.

@nspin

nspin commented Jul 17, 2026

Copy link
Copy Markdown
Member Author

I did however struggle to follow some of the logic on a first read through, particularly in the very large where clause of translate. I have the feeling that this would be easier to read and more maintainable if most of those helpers were separated out into their own functions with type annotations, but this almost definitely isn't worth doing now.

I did a bit of refactoring to pull the largest where-scoped functions out to the top level.

Introduces a new output format. This format is a JSON-serialized
representation of the spec, for consumption by the Rust implementation
of the CapDL initializer.

Co-authored-by: Ivan Velickovic <i.velickovic@unsw.edu.au>
Signed-off-by: Nick Spinale <nick@nickspinale.com>
@lsf37

lsf37 commented Jul 19, 2026

Copy link
Copy Markdown
Member

Eventually I'd like to add tests for this and also an automated cross-check if files produced by this tool can be read properly by the Rust side. But that can be in separate PRs.

Were you thinking of something more complicated, or just basic processing tests like we do with the examples in this repository? Something like that for this format would be nice, to at least make sure that other changes to the tool don't break things in unexpected ways.

For now just basic processing tests on the examples we already have.

Longer term, It'd be nice to generate specs and use them to cross-check the tools and loaders against each other, but that needs a bit of time to implement.

@lsf37 lsf37 left a comment

Copy link
Copy Markdown
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I'm happy with the changes. Will merge.

@lsf37
lsf37 merged commit f71ced8 into seL4:master Jul 19, 2026
11 checks passed
@github-project-automation github-project-automation Bot moved this from In Progress to Done in seL4 July'26 release (22 July) Jul 19, 2026
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

Haskell Haskell part of capDL

Projects

No open projects

Development

Successfully merging this pull request may close these issues.

3 participants