Add dependency to coq-elpi in coq-corn.dev

[MSoegtropIMC]

No description provided.

[MSoegtropIMC]

Since this is "dev" which has been called "pretty much wild west" before I will self merge as soon as CI passes unless someone protests until then.

[SkySkimmer]

Looks like elpi is failing

- File "theories/dune", line 5, characters 11-20:
- 5 |  (theories elpi_elpi))
-                ^^^^^^^^^
- Theory "elpi_elpi" has not been found.
- -> required by theory elpi in theories/dune:2
- -> required by theory elpi_examples in examples/dune:3
- -> required by _build/default/examples/example_abs_evars.vo
- -> required by
-    _build/install/default/lib/coq/user-contrib/elpi_examples/example_abs_evars.vo
- -> required by _build/default/coq-elpi.install
- -> required by alias install

cc @gares

[MSoegtropIMC]

@SkySkimmer : what I don't quite understand: elpi is on coq-ci - does fail there on its own as well?

[SkySkimmer]

I guess it's missing LPCIC/coq-elpi@069018b here

[MSoegtropIMC]

I guess it's missing LPCIC/coq-elpi@069018b here

This has been merged 2 days ago. How can it fail today lacking this?

[SkySkimmer]

because it's a opam file change so it needs to be copied to this repo ("here")

[gares]

Right, but I cannot do it today

[MSoegtropIMC]

because it's a opam file change so it needs to be copied to this repo ("here")

Ah yes, sorry.

Shall I piggy pack it to this PR?

[gares]

Yes please

[MSoegtropIMC]

Done.

[MSoegtropIMC]

I now get while building coq-elpi.dev:

# +  File "./test.v", line 1, characters 0-39:
# +  Error: Cannot load Stdlib.Strings.String: no physical path bound to
# +  Stdlib.Strings

@gares ?

[gares]

Looks like the dune files for the tests miss the stdlib dep. I Don't get why I did not figure it out upstream

[MSoegtropIMC]

Thanks! Please ping me as soon as the up stream fix is done.

[gares]

should work now

[MSoegtropIMC]

Thanks. I will rebase the PR to trigger a new CI.

[MSoegtropIMC]

@gares : So I guess the "stdlib-shims" need to remain and I should just remove the second commit from this PR?

[gares]

yes, please remove your second commit

[MSoegtropIMC]

As announced last Monday I self merge as soon as CI passes => merge.