analysis
analysis copied to clipboard
math-comp
Topological vector spaces
Motivation for this change
Adding topological vector spaces as a new structure. Further PRs will integrate the theory of topological vector spaces (duality, function spaces, characterization of topologies, distribution theory)
Checklist
- [x] added corresponding entries in
CHANGELOG_UNRELEASED.md
- [x] added corresponding documentation in the headers
Reference: How to document
Reminder to reviewers
- Read this Checklist
- Put a milestone if possible
- Check labels
For the record, a previous comment on PR#539, now closed by @zstone1 "With a long-term goal of doing spectral theory, I'm looking at defining integrals for a TVS. The most straightforward choice seems to be "weak integrals"."
The last commit makes the dev compile but it is clearly a temporary fix.
Rebasing the branch over mc-analysis 1.6.0, and in particular over the PR splitting topology in multiple files, makes the compilation fail. real.v does not find the splitted files when importing the topology. This seems to work in master on the CI. What is missing in the branch evt2?
Rebasing the branch over mc-analysis 1.6.0, and in particular over the PR splitting topology in multiple files, makes the compilation fail.
real.vdoes not find the splitted files when importing the topology. This seems to work in master on the CI. What is missing in the branchevt2?
I am not sure but that maybe because you have some Require Imports that do not start with From mathcomp even though the latter has been made mandatory by the use the -Q option instead of -R introduced by the PR 1348.
I encountered a possibly similar issue where a stray .vo file confusing the build. Doing a make clean doesn't remove .vo that correspond to deleted .v files. So you might still have theories/topology.vo that must be deleted manually.
In such cases, I tend to use git clean -dxf . (be sure to check the output of the dry run git clean -dxn . before)
