Jason Gross

And in this extended file: ```coq (* -*- mode: coq; coq-prog-args: ("-emacs" "-w" "-deprecated-native-compiler-option,-native-compiler-disabled" "-native-compiler" "ondemand" "-R" "." "IsomorphismChecker" "-top" "IsomorphismChecker.DemoChecker") -*- *) (* File reduced by coq-bug-minimizer from original...

I have created #527 for the .v file part. I am not sure how to install the .glob files, as it seems they are not even fully generated by the...

> > Note that coq_makefile-made makefiles install the .v and .glob files: > > I dodn't know about this convention. Flocq doesn't install .glob files, for instance. > Flocq seems...

> Some target-dependent modules have multiple implementations in different directories, but only one is compiled. Ah, I see, that makes sense. I was assuming things based just on the directory...

Has it been resolved?

https://github.com/Homebrew/homebrew-core/pull/193315 is still open ...

Seems wrong...

Probably the right thing to do here is to rip out the existing libfilename logic and just parse the output of `echo 'Print LoadPath.' | coqtop`

I guess I need to fix the tests ``` __________________________ test_log_softmax_noneaxis ___________________________ [gw1] linux -- Python 3.10.13 /opt/hostedtoolcache/Python/3.10.13/x64/bin/python scipy/special/tests/test_log_softmax.py:58: in test_log_softmax_noneaxis assert_allclose(sc.log_softmax(x), expected, rtol=1e-13) expected = array([[-3.4401897, -2.4401897], [-1.4401897, -0.4401897]])...

Is there a good way to test only this one file, in light of `python dev.py test -v` failing?