Facundo Domínguez

For reference, an issue discussing uniques and unique tags in GHC: https://gitlab.haskell.org/ghc/ghc/-/issues/26264

Thanks Claudio. > Well, yes. On MacOS there is xcode and its tightly integrated into the system. 👍 I just found related explanations in the nixpkgs_cc_configure [documentation](https://github.com/tweag/rules_nixpkgs?tab=readme-ov-file#nixpkgs_cc_configure). > What's a...

Thanks @avdv! > One needs to move loading the rules_nixpkgs' toolchain repositories before calling rules_haskell_dependencies() Alas, this makes `rules_haskell` and `rules_nixpkgs` so difficult to configure. I hope bazel modules help...

I measured with wall clock time. The improvements are less pronounced there. Still there are some reasons that incline me to remove `--cores`. 1. None of the speedups due to...

Yes, we could do that, but note that it doesn't address any of the issues I'm bringing. If there were some use case that badly needs support for multiple cores,...

The implementation in LH is small and easy to reinstate with `git revert 3f27e04d`. I think the pitfalls in the implementation make your point (a) a very narrow possibility at...

I changed the default to only 1 core in #2564.

I think multiple processes are created. [Here's](https://github.com/ucsd-progsys/liquid-fixpoint/blob/develop/src/Language/Fixpoint/Solver.hs#L117) where the implementation splits for multicore. My impression is that much effort is spent in serializing expressions to SMTLIB for every core. But...

Thanks for the report. It is telling that renaming `y` to `z` in the type of `addByProxy'` makes verification pass.

``` ∀s ∈ map proj₂ ((txscripts txw utxo) ∩ (neededHashes × Scriptᵖʰ¹)) ``` Another attempt. After a few corrections it doesn't look particularly better anymore to me :) ``` ∀s...