Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

port to math-comp 2 + vertical cell repo + flavor branch #36

Closed
wants to merge 43 commits into from
Closed

port to math-comp 2 + vertical cell repo + flavor branch #36

wants to merge 43 commits into from

Conversation

gares
Copy link
Member

@gares gares commented Apr 22, 2024

No description provided.

@affeldt-aist
Copy link
Member

the only file that does not compile yet with MathComp 2 is xssralg.v
but it contains a redefinition of an ordered type so maybe it is not necessary anymore? @ybertot

@affeldt-aist
Copy link
Member

@gares @t6s maybe we can merge this PR and make this our working environment?

@affeldt-aist
Copy link
Member

(the opam file should be ok leading to a green CI)

@affeldt-aist
Copy link
Member

squash and merge somebody? @ybertot

@affeldt-aist affeldt-aist changed the base branch from master to flavor April 24, 2024 06:06
@affeldt-aist affeldt-aist changed the base branch from flavor to master April 24, 2024 06:07
@affeldt-aist affeldt-aist changed the title port to math-comp 2 port to math-comp 2 + vertical cell repo + favor branch Apr 24, 2024
@affeldt-aist affeldt-aist changed the title port to math-comp 2 + vertical cell repo + favor branch port to math-comp 2 + vertical cell repo + flavor branch Apr 24, 2024
thery and others added 22 commits April 26, 2024 03:13
@thery
load and save button
6eaa71c
@thery
fix modality in graph display
651a4c8
@ybertot
changes of notations, and underE and strictE work on the concept
cd210d1 
definied in points_and_edge instead of generic_trajectories
@affeldt-aist
bool -> Prop
6e4a54f
@ybertot
reinstate the separation between the abstract presentation of shortes…
96e7b3a 
…t_path

and the rest of generic_trajectories.  adds a new function to be extracted
so that we can visualize the piecewise linear trajectory
@ybertot
rename Qpoint_to_point into Qstraight_point_to_point
acac84a
@thery
Adding straight line
d73e8ab
@thery
fix refresh position
0c98981
@ybertot
use call_straight at the right place
ade4804
@ybertot
straight line trajectories in blue
34a3360
@ybertot
add some form of improvement for straight trajectories
5f34171
@ybertot
adds slides for the Festschrift
02deb90
@ybertot
silence
f2f42a1
@ybertot
changed the order in which the points are are stored in right_pts,
060bc02 
The proofs go through, but the algorithm is broken, because updating
right_pts in the case of vertically aligned events is now wrong.
@ybertot
change the order of points in update_closed_cell
812c7d1
@ybertot
introducing the invariant for non-general positions (with possibly
0ca511f 
vertically aligned events)
@ybertot
adds information about publications
dde8ba2
@ybertot
attempt with more notations
ec8991e
@ybertot
last improvements before the talk
3b91293
@ybertot
finished proving the common invariant for update_open_cell
57b7a67
@ybertot
proved that update_open_cell satisfies the common_non_gp_invariant
21f975d
@ybertot
replace seq_subst by an implementation based on map
ef307d3
@ybertot ybertot deleted the branch master October 30, 2024 15:31
@ybertot ybertot closed this Oct 30, 2024
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Reviewers
No reviews
Assignees
No one assigned
Labels
None yet
Projects
None yet
Milestone
No milestone
Development

Successfully merging this pull request may close these issues.
4 participants
@gares @affeldt-aist @ybertot @thery