adampetcher / fcf Goto Github PK

There are a lot of deprecation warnings when compiling FCF with Coq 8.16. It might be worth fixing these, to save trouble in the future.

@adampetcher What's the current status of FCF? I see recent additions by @JasonGross, @andres-erbsen and @natelaunchbury.
Are there other projects using FCF?

As described in PrincetonUniversity/VST#290, the use of Qed when creating typeclass instances makes it so that you can't evaluate expressions using the typeclass:

Compute 1 ?= 1.
     = (let (eqb, _) := nat_EqDec in eqb) 1 1

The instances in EqDec.v that currently end in Qed and shoulde be changed to Defined are:

• Vector_EqDec
• unit_EqDec
• bool_EqDec
• nat_EqDec
• option_EqDec
• list_EqDec

COQC Rat.v
File "./Rat.v", line 188, characters 2-26:
Error: Found no subterm matching "(x * n1)%nat" in the current goal.

We need to fix the following copyright and license issues:

1. Give attribution and copyright ownership to contributors. At present, everything is still marked as copyright Adam Petcher
2. It may be best to remove dates and ownership from each source file and only include a header to the LICENSE file.
3. Update the dates. After 2 above is complete, this should only affect the LICENSE file.

In various tactics such as fcf_skip, the use of "intuition" leads to this warning in Coq 8.17:

Warning:
"auto with *" was used through the default "intuition_solver" tactic.
This will be replaced by just "auto" in the future.

The quick-and-dirty way to fix this is to replace intuition with intuition auto with *. The cleaner way to fix it is intuition auto with XXX where XXX is the set of hint databases you really need.

`I would prefer to keep the non-building files in the repo for the following reasons:

They still can be useful illustrations (especially the examples).
There may be some argument in there that is needed in the future, and it would be easier to fix the file than to develop it from scratch. A person probably wouldn't think to look in the history for "almost working" theory.
That being said, some of the non-building files are definitely old junk that needs to be removed. So I suggest:

Leave these files in and exclude them from the build. If you like, you can move the non-building files to a separate directory to simplify the build.
Create a ticket (assigned to me) reminding me to go through and clean up these broken files. Useless ones should be removed, valuable ones should be fixed.` @adampetcher

The files are now under src/FCF/Broken, with non-building bits commented out.

Since FCF is useful and seems to have at least one maintainer (for example, @andres-erbsen), I suggest that FCF should be released via opam in the coq-released archive, and then added to the Coq Platform.

• To add this to coq-released, you make a fork of https://github.com/coq/opam and then submit a pull request.
• Once that is done and accepted, you can nominate FCF for inclusion in the Coq Platform. That is a set of libraries that, in each release every 6-12 months, are all guaranteed compatible with each other (to avoid "dependency hell"). Then the Coq Platform board decides whether FCF satisfies the criteria.

Does anyone else think this is a good idea, and is anybody willing to be a "maintainer" for the purposes of this process? If so, there's at least one member of the Coq Platform board who will advocate for it.

I'm working on a class project to use FCF to prove some things about the Luby-Rackoff construction (basically section 6 from the following paper http://www.shoup.net/papers/games.pdf).

I'm not sure about the purpose of getSupport but I see that it is used in a lot of places. Can you provide a description?

Thanks!

Erik

Since Coq 8.13 (plus or minus), the Instance and Hint Resolve require a locality annotation, such as Global or Local or #[export]. Without the annotation, one gets a deprecation warning message. Here's an example from compiling FCF in Coq 8.15.1:

File ".\fcf/src/FCF/EqDec.v", line 387, characters 0-62:
Warning: The default value for instance locality is currently "local" in a      
section and "global" otherwise, but is scheduled to change in a future
release. For the time being, adding instances outside of sections without       
specifying an explicit locality attribute is therefore deprecated. It is        
recommended to use "export" whenever possible. Use the attributes #[local],     
#[global] and #[export] depending on your choice. For example: "#[export]       
Instance Foo : Bar := baz." [deprecated-instance-without-locality,deprecated]

For strict compatibility with previous FCF behavior, you would add Global before each such Instance or Hint. But I would suggest instead using #[export]. For clients that do Require Import, there will be no difference. Clients that do Require without Import will be affected. Anyway, one way or another I would like to stop seeing these deprecation messages.

Currently, a project using FCF as a module gets all FCF filenames in the root namespace, e.g.
"Require Import Asymptotic" refers to FCF-s notion of asymptotic, and effectively prevents use of any library of the same name. I think it would make sense to change FCF _Coqproject to -R . FCF. In that case importers would need to type "Require Import FCF.Asymptotic". Should I go do it and make a PR?

I was trying to use IND_CPA_SecretKey_equiv from Encryption_2W.v, but building Encryption_2W.v seems to fail on the line:
Context {EncryptionScheme_SecretKey}`.

I couldn't find EncryptionScheme_SecretKey in the file directory or the Git commit history. Looks like it was never committed? What would need to be done to get this file to compile?

Since omega is now deprecated, it would be a good idea to use lia everywhere instead.

Hello,

I am considering using this library in a project, and I noticed that this repository does not seem to contain any information about copyright/patent licensing. https://github.com/PrincetonUniversity/VST/blob/master/LICENSE says that its imported copy of fcf is released under the 2-clause BSD license. If this is also true for this repository, please

1. Add a corresponding license file into the root directory of the project (e.g., from https://github.com/IQAndreas/markdown-licenses/blob/master/bsd-2.md)

2. Add a short license header to each file (possibly using the 10-line shell script from https://stackoverflow.com/questions/151677/tool-for-adding-license-headers-to-source-files), for example

   (* Copyright 2010 <AUTHOR>.  All rights reserved.
    * Use of this source code is governed by a BSD-style
    * license that can be found in the LICENSE file. *)
   

3. (patents) if something similar to https://golang.org/PATENTS is true about this project as well, add a corresponding statement to a corresponding file. This is not implied by the BSD-2 license, and some may be comfortable using this code without it, but IMHO it is easier to add the statement (if it is true) than to convince somebody's employer that they don't need it to use the code.

The options I outlined here are almost straight from http://choosealicense.com/, you can see there for more information and alternatives.

Thanks,
Andres

If you like, you can remove the entire ESPADA directory. I don't plan to maintain this proof. If you do this, create a ticket (assigned to me) reminding me to look through this proof and see if there is any useful theory that should be extracted. @adampetcher