Comments (15)
What can I start from?
I did a tentative split as PR #57 .
It turns out that some files that are not explicitly depending on probabilities still depend on infotheo for some utilities.
Dependencies on classical_sets_ext.v
could be removed by PRing the needed lemmas to mathcomp-analysis.
As for dependencies on ssr_ext.v
and ssrZ.v
, it is not obvious how to proceed to me right now.
from monae.
Therefore, I guess, the solution would be to put
ssrZ
(and, perhaps,ssrR
) into a separate small self-contained library?
In this case, the strategy would be to have a new subdirectory in infotheo for these two libraries
and release infotheo as two opam packages (like it is done for MathComp)? (@t6s, is it ok with you?)
Sounds good!
Would you like to do it by yourself?
Otherwise, I can try to prepare a PR in the coming days.
You may want to PR it because I will lack time in the next few days. :-(
from monae.
Keep infotheo for the main package and ssrstd for ssrZ+ssrR (because it provides ssr-like naming for standard library's datatypes)?
ssrstd sounds too generic or strong, doesn't it? What about thinssr or thinssrstd?
Another proposal from riot: ssrwrap-stdnum @garrigue
Note that there is https://github.com/math-comp/mczify/blob/master/theories/ssrZ.v
that we could maybe try to reuse instead of spinning off another version of ssrZ.v.
from monae.
Thank you for your interest!
monae uses infotheo for probabilities and infotheo uses fields for error-correcting codes (in a limited way) iirc,
hence the dependency on mathcomp-field
, which triggers the dependency on other MathComp packages.
(So splitting the probability
subdirectory out of infotheo might also be another option to reduce
dependencies, though fields are likely to get back through mathcomp-analysis
unless it is also split.)
Note also that monae's master now uses Hierarchy Builder and this triggers a new set of dependencies
that are here to stay given the benefits of using Hierarchy Builder (whose recent introduction in monae
improved its usability).
The main reason we didn't do any splitting so far is essentially lack of time and also because
changes in mathcomp-analysis
often trigger changes in infotheo
and in turn in monae
.
I suspect that this situation will continue in the near future because of the introduction of
Hierarchy Builder in MathComp and because we have plans to extend monae that depend
on mathcomp-analysis
.
I fear that splitting packages further might make this migration more tedious for us by
requiring even more releases. It might be more efficient to perform it after the situation with
Hierarchy Builder has stabilized.
I didn't know the depopts
feature of opam but right now it sounds to me like the most reasonable
option (at least given the resources on our side).
from monae.
I am afraid that, after the merger of monae-hb branch, even the core part now suffers from a heavy dependency starting from Hierarchy Builder.
from monae.
You can also observe that the subdirectory impredicate_set
contains a subset of monae (code is duplicated almost verbatim) without the probabilities-related stuff (because in the current state of affairs it is not compatible with the impredicative set option).
from monae.
Hi @affeldt-aist, thank you for the quick response!
Note also that monae's master now uses Hierarchy Builder and this triggers a new set of dependencies
that are here to stay given the benefits of using Hierarchy Builder.
I guess dependencies on coq-mathcomp-ssreflect
and coq-hierarchy-builder
are fine. Both packages are basic infrastructure of mathcomp
style Coq proofs.
I didn't know the depopts feature of opam but right now it sounds to me like the most reasonable
option.
Thereby, I think the problem can be solved in two steps.
(1) Split the project "internally", use depopts
to conditionally enable more advanced features of the library.
(2) Once the Hierarchy Builder and other dependency packages will stabilize, split the monae
repo. In the best-case scenario, at this point the repo already be split into subparts, that would be built in several stages with the help of depopts
, so the migration to several monae
subpackages should go smoothly.
You can also observe that the subdirectory impredicate_set contains a subset of monae (code is duplicated almost verbatim) without the probabilities-related stuff
Do you think the problem with the code duplication should also be solved as a subtask of this issue?
With respect to the solution of this issue, I would really be happy to help here. What can I start from?
Moving the probability monad out of hierarchy.v
and unification of hierarchy.v
with impredicative_set/ihierarchy.v
seems like a reasonable first step. Should I start from it, or do you have another plan in mind?
from monae.
What can I start from?
I did a tentative split as PR #57 .
Dependencies onclassical_sets_ext.v
could be removed by PRing the needed lemmas to mathcomp-analysis.
As for dependencies onssr_ext.v
andssrZ.v
, it is not obvious how to proceed to me right now.
I've removed some unused dependencies on infotheo in #59
As for the real dependencies that are still there, I've noticed the following:
-
monad_model.v
depends onclassical_sets_ext.bigcup_
lemmas and alsoconvex.choice_of_Type
. The latter I suppose can be moved toboolp.v
frommathcomp-analysis
in a separate PR. -
example_nquees.v
andexample_array.v
depend oneqType
instance forZ
(ssrZ.Z_eqType
).
trace_lib.v
also depends on some notations forZ
fromssrZ
.
However, my general question was why the vanilla CoqZ
is used instead ofssrint
?
It looks like the latter supports exactly the same functionality as required bymonae
. -
example_quicksort.v
uses bounded sequences fromssr_ext
. It is in fact the single usage ofssr_ext
.
Although it looks like it is still WIP, so one possible temporary solution would be just not to build it?
Another solution would be to try PRbseq
tomathcomp
.
from monae.
I've removed some unused dependencies on infotheo in #59
Thank you for the careful review!
As for the real dependencies that are still there, I've noticed the following:
1. `monad_model.v` depends on `classical_sets_ext.bigcup_` lemmas and also `convex.choice_of_Type`.
The latter I suppose can be moved to
boolp.v
frommathcomp-analysis
in a separate PR.
Let's do that (math-comp/analysis#405, math-comp/analysis#406).
2. `example_nquees.v` and `example_array.v` depend on `eqType` instance for `Z` (`ssrZ.Z_eqType`). `trace_lib.v` also depends on some notations for `Z` from `ssrZ`. However, my general question was why the vanilla Coq `Z` is used instead of `ssrint`? It looks like the latter supports exactly the same functionality as required by `monae`.
We've been using Z instead of ssrint because it is a bit easier to use (in particular, more people are familiar with it),
it lends itself to execution (in particular, it is useful to test examples), and it also appears naturally when using the
reals from the Coq standard library.
3. `example_quicksort.v` uses bounded sequences from `ssr_ext`. It is in fact the single usage of `ssr_ext`. Although it looks like it is still WIP, so one possible temporary solution would be just not to build it? Another solution would be to try PR `bseq` to `mathcomp`.
Actually, we will soon merge an admit-free version (https://github.com/AyumuSaito/monae/tree/saito_quicksort).
After this merge, some generic lemmas will certainly make there way to lib files and afterwards there will be more
work on the same line to enrich the array monad. So we'd rather like to keep it in master.
Maybe we should go with PRing bseq to mathcomp for this one. It is definitely useful in monae and should
be useful for coding (although it is under exploited in infotheo as of today).
from monae.
We've been using Z instead of ssrint because it is a bit easier to use (in particular, more people are familiar with it),
it lends itself to execution (in particular, it is useful to test examples), and it also appears naturally when using the
reals from the Coq standard library.
Therefore, I guess, the solution would be to put ssrZ
(and, perhaps, ssrR
) into a separate small self-contained library?
Maybe we should go with PRing bseq to mathcomp for this one. It is definitely useful in monae and should
be useful for coding (although it is under exploited in infotheo as of today).
Sounds good!
Would you like to do it by yourself?
Otherwise, I can try to prepare a PR in the coming days.
from monae.
In this case, the strategy would be to have a new subdirectory in infotheo for these two libraries
and release infotheo as two opam packages (like it is done for MathComp)? (@t6s, is it ok with you?)
Okay to separate the package into two. But what would you name them?
infotheo-ssrext and infotheo-infotheo?
from monae.
Okay to separate the package into two. But what would you name them?
infotheo-ssrext and infotheo-infotheo?
Keep infotheo for the main package and ssrstd for ssrZ+ssrR (because it provides ssr-like naming for standard library's datatypes)?
from monae.
Keep infotheo for the main package and ssrstd for ssrZ+ssrR (because it provides ssr-like naming for standard library's datatypes)?
ssrstd sounds too generic or strong, doesn't it? What about thinssr or thinssrstd?
from monae.
Keep infotheo for the main package and ssrstd for ssrZ+ssrR (because it provides ssr-like naming for standard library's datatypes)?
ssrstd sounds too generic or strong, doesn't it? What about thinssr or thinssrstd?
Another proposal from riot: ssrwrap-stdnum @garrigue
from monae.
Let's do that (math-comp/analysis#405, math-comp/analysis#406).
fyi, those two have been merged
from monae.
Related Issues (20)
- document factories
- factory to buil monads from adjoint functors
- Adding monadic fixpoint to define Mu's quicksort
- freshMonad should inherit failR0
- Remove when available from analysis
- Avoid explicit definition of aliases with HB
- generalize bind law
- code duplicated in infotheo
- model of array monad HOT 1
- reduce dependency wrt infotheo HOT 1
- notation broken
- global notation
- try using ssrint HOT 1
- typo in Record isMonadArray
- document liftM2
- remove notation
- move to better location
- remove file? HOT 1
- non forgetful inheritance detected
Recommend Projects
-
React
A declarative, efficient, and flexible JavaScript library for building user interfaces.
-
Vue.js
🖖 Vue.js is a progressive, incrementally-adoptable JavaScript framework for building UI on the web.
-
Typescript
TypeScript is a superset of JavaScript that compiles to clean JavaScript output.
-
TensorFlow
An Open Source Machine Learning Framework for Everyone
-
Django
The Web framework for perfectionists with deadlines.
-
Laravel
A PHP framework for web artisans
-
D3
Bring data to life with SVG, Canvas and HTML. 📊📈🎉
-
Recommend Topics
-
javascript
JavaScript (JS) is a lightweight interpreted programming language with first-class functions.
-
web
Some thing interesting about web. New door for the world.
-
server
A server is a program made to process requests and deliver data to clients.
-
Machine learning
Machine learning is a way of modeling and interpreting data that allows a piece of software to respond intelligently.
-
Visualization
Some thing interesting about visualization, use data art
-
Game
Some thing interesting about game, make everyone happy.
Recommend Org
-
Facebook
We are working to build community through open source technology. NB: members must have two-factor auth.
-
Microsoft
Open source projects and samples from Microsoft.
-
Google
Google ❤️ Open Source for everyone.
-
Alibaba
Alibaba Open Source for everyone
-
D3
Data-Driven Documents codes.
-
Tencent
China tencent open source team.
from monae.