Tim Hutt

Expose instruction encoding, CSR bitfield information as JSON

13

Currently there isn't an easy way to extract useful information from the Sail model like: * Instruction encoding patterns * Instruction assembly format * CSR field information This information is...

Refactor PTE update code & fix reachable assertion

2

Deduplicate the code to write the PTE, and in the process remove the reachable (I think) assertion "invalid physical address in TLB". It actually ended up being basically the same...

The virtual memory code has an assertion `"invalid physical address in TLB"` that happens when you have a TLB hit, and the PTE A/D bits need to be updated, and...

We discussed this a little [here](https://github.com/riscv/sail-riscv/pull/615/files#diff-20961e085e0ef6d48e592b88ce9ce59cce9018a99fd202615c3aabd8729bcf71), but I think `PC` should be a `virtaddr` rather than `xlenbits` like it currently is.

Reservation is done on physical addresses, so these should take `physaddr` not `xlenbits`.

`unknown version` when bootstrapping Rye

2

### Steps to Reproduce ``` nix-channel --add https://nixos.org/channels/nixos-24.05 nixpkgs nix-channel --update nix-shell -p rye --command "rye test" ``` ### Expected Result It works. ### Actual Result ``` Bootstrapping rye internals...

Extra help for 0 * m = m

2

I got a bit stuck on [this level](https://adam.math.hhu.de/#/g/leanprover-community/nng4/world/Multiplication/level/2). Probably missing something obvious but you might want to add a "show more help" for it. It doesn't seem like there is...

Level completed with warnings?

2

On [this level](https://adam.math.hhu.de/#/g/leanprover-community/nng4/world/LessOrEqual/level/6) I somehow managed to complete it, but it says "Level completed with warnings".  ``` cases hxy with a ha cases hyx with b hb rw [ha]...

Exposing trait methods to C++

1

We can expose a trait object to C++ something like this: ```rust trait MyData { fn get_data(&self) -> Result; } type DynMyData = Box; #[cxx::bridge] mod ffi { extern "Rust"...

Fails in Mac CI

6

I have this running in Github actions on Mac: ``` - name: Install cargo-binstall uses: cargo-bins/cargo-binstall@main - name: Install Maturin run: cargo binstall maturin ``` But it fails with `403...