Josselin Poiret

The ip command is used, which belongs to the iproute project, but is not listed as a dependency.

System32's dbgeng.dll is always used for debugging.

18

**Describe the bug** Although I can connect fine to a WinDbg session running on the computer using another WinDbg client, Ghidra cannot do the same: the GADP window flashes for...

Duplication of code in the library

5

I've been noticing quite a lot of code that's duplicated in the library recently, so I think we could create a main issue for all such cases that we can...

Add workflow with Agda master.

1

Hi, this is a first try at adding a CI workflow using Agda master, without rebuilding it ourselves. It simply fetches the nightly release and uses that instead. This seems...

Presheaf definition leads to unsolved metavariable for base category

3

Hi everyone, Since `Presheaf C ...` is defined as `Functor (C ^op) (SETS ...)`, `C` can't be inferred from an argument `P : Presheaf C ...`. This is because Agda...

Add documentation generation

1

This uses the manpage XSL and asciidoc config files from git 2.40.1 to build the documentation on its own. This work was done to package this in GNU Guix, inspired...

Fix archflag added to CFLAGS instead of CXXFLAGS

2

The default behaviour of AX_GCC_ARCHFLAG is to append the archflag to CFLAGS, so we instead set CXXFLAGS with the right value.

Feature request: explicit sorts in notations

2

### Is your feature request related to a problem? With the following sort-poly equality ```coq Inductive eq@{s s'|u|} {A : Type@{s|u}} (a : A) : A -> Type@{s'|u} := refl...

Wrong relevance mark when rewriting with sort-poly equality

2

### Description of the problem The below example fails with "Binder (P : "A -> Type") has relevance mark set to a variable α1190 but was expected to be relevant...

### Description of the problem Minimization fails to infer the more precise `Prop` when `Prop` and `Type` are possible, as in the below example. ### Small Coq file to reproduce...