Mauricio Collares

∀-× (Quantifiers): Is plfa.Isomorphism.extensionality enough?

7

If I try to prove ∀-distrib-× using the same proof for from∘to as I did in →-distrib-× (using plfa.Isomorphism.extensionality), I get the following somewhat confusing error message in Agda 2.5.4.1:...

chore(lp): fix compilation error

2

``` /build/source/src/util/lp/permutation_matrix.h:126:44: error: cannot convert 'const std::vector' to 'unsigned int*' in return 126 | unsigned * values() const { return m_permutation; } | ^~~~~~~~~~~~~ | | | const std::vector ```...

### Prerequisites * [x] Put an X between the brackets on this line if you have done all of the following: * Checked that your issue isn't already [filed](https://github.com/leanprover-community/lean/issues). *...

### Prerequisites * [x] Put an X between the brackets on this line if you have done all of the following: * Checked that your issue isn't already [filed](https://github.com/leanprover-community/lean/issues). *...

"make check" requires network access (4.12.0)

6

Since #4652, `IsomorphismGroups` uses `atlasrep` via `IsomorphismSimpleGroups`. This makes the install test at https://github.com/gap-system/gap/blob/v4.12.0/tst/testinstall/grp/basic.tst#L488 hit the network to download [a script](http://atlas.math.rwth-aachen.de/Atlas/spor/M22/words/M22G1-find1). Maybe setting `NoPrecomputedData` is an acceptable solution for install...

This is with Clang 11. See #284 for an older version of this problem. ``` clang++ -DHAVE_CONFIG_H -I. -I.. -I.. -O2 -march=native -Wall -DNDEBUG -UDEBUG -I/nix/store/z69w4bjiqzdfkaqryvzqxqfw1aa31nbb-givaro-4.2.0/include -g -c -o test-simd.o...

crashes in `test-{smith-form-valence,regression}` compiling with `-D_FORTIFY_SOURCE=3`

5

NixOS now builds all packages with [`-D_FORTIFY_SOURCE=3`](https://developers.redhat.com/articles/2022/09/17/gccs-new-fortification-level). This causes two tests, `test-smith-form-valence` and `test-regression`, to fail with buffer overflows. To avoid duplication, I will only post the relevant details for...

AudioBufferSourceNode: Implement linear extrapolation for endpoints

2

buffer-resampling.html (WPT test) fails because we interpolate the last sample with 0 when we output a sample with pos corresponding to buffer.len() - 1 < pos < buffer.len(). For playhead...

AudioParam: Running only one event per tick leads to off-by-one event_start_time

2

Consider the following line, from WPT (the-audioparam-interface/audioparam-method-chaining.html): ``` envelope.gain .setValueAtTime(0.0, 0.0) .linearRampToValueAtTime(1.0, 1.0); ``` If I understand correctly, setValueAtTime runs at tick 0. We only process one event per tick,...

Start()'s when parameter should be ignored if it's in the past. We currently use a simple heuristic in process() to determine if it should be ignored, but by the time...