summaryrefslogtreecommitdiffstats
path: root/fs/eventfd.c
AgeCommit message (Expand)Author
2017-03-02sched/headers: Prepare to move signal wakeup & sigpending methods from <linux...Ingo Molnar
2016-03-22eventfd: document lockless access in eventfd_pollPaolo Bonzini
2015-12-08Documentation: filesystem: Fix typo in fs/eventfd.cMasanari Iida
2015-02-17eventfd: don't take the spinlock in eventfd_pollChris Mason
2014-11-05fs: Convert show_fdinfo functions to voidJoe Perches
2014-01-25eventfd_ctx_fdget(): use fdget() instead of fget()Al Viro
2012-12-17fs, eventfd: add procfs fdinfo helperCyrill Gorcunov
2012-05-31eventfd: change int to __u64 in eventfd_signal()Sha Zhengju
2012-02-28fs: reduce the use of module.h wherever possiblePaul Gortmaker
2011-02-21Docbook: add fs/eventfd.c and fix typos in itRandy Dunlap
2010-10-15llseek: automatically add .llseek fopArnd Bergmann
2010-03-30include cleanup: Update gfp.h and slab.h includes to prepare for breaking imp...Tejun Heo
2010-01-25eventfd - allow atomic read and waitqueue removeDavide Libenzi
2009-12-22anonfd: Allow making anon files read-onlyRoland Dreier
2009-09-23anonfd: split interface into file creation and installDavide Libenzi
2009-06-30eventfd: revised interface and cleanupsDavide Libenzi
2009-06-12eventfd: export eventfd_signal and eventfd_fget for lguestRusty Russell
2009-04-01epoll keyed wakeups: make eventfd use keyed wakeupsDavide Libenzi
2009-04-01eventfd: improve support for semaphore-like behaviorDavide Libenzi
2009-01-14[CVE-2009-0029] System call wrappers part 32Heiko Carstens
2008-07-24flag parameters: check magic constantsUlrich Drepper
2008-07-24flag parameters: NONBLOCK in eventfdUlrich Drepper
2008-07-24flag parameters: eventfdUlrich Drepper
2008-07-24flag parameters: anon_inode_getfd extensionUlrich Drepper
2008-05-01[PATCH] sanitize anon_inode_getfd()Al Viro
2008-02-06fs/eventfd.c should #include <linux/syscalls.h>Adrian Bunk
2007-05-18eventfd use waitqueue lock ...Davide Libenzi
2007-05-11signal/timer/event: eventfd coreDavide Libenzi
generated by cgit v1.2.3 (git 2.25.1) at 2024-08-28 11:08:28 +0000
'>113 114 115 116 117 118 119 120 121 122 123 124 125 126 127 128 129 130 131 132 133 134 135 136 137 138 139 140 141 142 143 144 145 146 147 148 149 150 151 152 153 154 155 156 157 158 159 160 161 162 163 164 165 166 167 168 169 170 171 172 
# - coqide compilation can be disabled by setting buildIde to false
# - The csdp program used for the Micromega tactic is statically referenced.
#   However, coq can build without csdp by setting it to null.
#   In this case some Micromega tactics will search the user's path for the csdp program and will fail if it is not found.
# - The exact version can be specified through the `version` argument to
#   the derivation; it defaults to the latest stable version.

{ stdenv, fetchFromGitHub, writeText, pkgconfig
, ocamlPackages, ncurses
, buildIde ? !(stdenv.isDarwin && stdenv.lib.versionAtLeast version "8.10")
, glib, gnome3, wrapGAppsHook
, darwin
, csdp ? null
, version
}:

let
  sha256 = {
   "8.5pl1"    = "1976ki5xjg2r907xj9p7gs0kpdinywbwcqlgxqw75dgp0hkgi00n";
   "8.5pl2"    = "109rrcrx7mz0fj7725kjjghfg5ydwb24hjsa5hspa27b4caah7rh";
   "8.5pl3"    = "15c3rdk59nifzihsp97z4vjxis5xmsnrvpb86qiazj143z2fmdgw";
   "8.6"       = "148mb48zpdax56c0blfi7v67lx014lnmrvxxasi28hsibyz2lvg4";
   "8.6.1"     = "0llrxcxwy5j87vbbjnisw42rfw1n1pm5602ssx64xaxx3k176g6l";
   "8.7.0"     = "1h18b7xpnx3ix9vsi5fx4zdcbxy7bhra7gd5c5yzxmk53cgf1p9m";
   "8.7.1"     = "0gjn59jkbxwrihk8fx9d823wjyjh5m9gvj9l31nv6z6bcqhgdqi8";
   "8.7.2"     = "0a0657xby8wdq4aqb2xsxp3n7pmc2w4yxjmrb2l4kccs1aqvaj4w";
   "8.8.0" = "13a4fka22hdxsjk11mgjb9ffzplfxyxp1sg5v1c8nk1grxlscgw8";
   "8.8.1" = "1hlf58gwazywbmfa48219amid38vqdl94yz21i11b4map6jfwhbk";
   "8.8.2" = "1lip3xja924dm6qblisk1bk0x8ai24s5xxqxphbdxj6djglj68fd";
   "8.9.0" = "1dkgdjc4n1m15m1p724hhi5cyxpqbjw6rxc5na6fl3v4qjjfnizh";
   "8.9.1" = "1xrq6mkhpq994bncmnijf8jwmwn961kkpl4mwwlv7j3dgnysrcv2";
   "8.10.0" = "138jw94wp4mg5dgjc2asn8ng09ayz1mxdznq342n0m469j803gzg";
   "8.10.1" = "072v2zkjzf7gj48137wpr3c9j0hg9pdhlr5l8jrgrwynld8fp7i4";
   "8.10.2" = "0znxmpy71bfw0p6x47i82jf5k7v41zbz9bdpn901ysn3ir8l3wrz";
   "8.11.0" = "1rfdic6mp7acx2zfwz7ziqk12g95bl9nyj68z4n20a5bcjv2pxpn";
   "8.11.1" = "0qriy9dy36dajsv5qmli8gd6v55mah02ya334nw49ky19v7518m0";
   "8.11.2" = "0f77ccyxdgbf1nrj5fa8qvrk1cyfy06fv8gj9kzfvlcgn0cf48sa";
   "8.12+beta1" = "0jbm8am9j926s0h4fi0cjl95l37l6p7i03spcryyrd4sg5xrddr7";
  }.${version};
  coq-version = stdenv.lib.versions.majorMinor version;
  versionAtLeast = stdenv.lib.versionAtLeast coq-version;
  ideFlags = stdenv.lib.optionalString (buildIde && !versionAtLeast "8.10")
    "-lablgtkdir ${ocamlPackages.lablgtk}/lib/ocaml/*/site-lib/lablgtk2 -coqide opt";
  csdpPatch = if csdp != null then ''
    substituteInPlace plugins/micromega/sos.ml --replace "; csdp" "; ${csdp}/bin/csdp"
    substituteInPlace plugins/micromega/coq_micromega.ml --replace "System.is_in_system_path \"csdp\"" "true"
  '' else "";
self = stdenv.mkDerivation {
  pname = "coq";
  inherit version;

  passthru = {
    inherit coq-version;
    inherit ocamlPackages;
    # For compatibility
    inherit (ocamlPackages) ocaml camlp5 findlib num;
    emacsBufferSetup = pkgs: ''
      ; Propagate coq paths to children
      (inherit-local-permanent coq-prog-name "${self}/bin/coqtop")
      (inherit-local-permanent coq-dependency-analyzer "${self}/bin/coqdep")
      (inherit-local-permanent coq-compiler "${self}/bin/coqc")
      ; If the coq-library path was already set, re-set it based on our current coq
      (when (fboundp 'get-coq-library-directory)
        (inherit-local-permanent coq-library-directory (get-coq-library-directory))
        (coq-prog-args))
      (mapc (lambda (arg)
        (when (file-directory-p (concat arg "/lib/coq/${coq-version}/user-contrib"))
          (setenv "COQPATH" (concat (getenv "COQPATH") ":" arg "/lib/coq/${coq-version}/user-contrib")))) '(${stdenv.lib.concatStringsSep " " (map (pkg: "\"${pkg}\"") pkgs)}))
      ; TODO Abstract this pattern from here and nixBufferBuilders.withPackages!
      (defvar nixpkgs--coq-buffer-count 0)
      (when (eq nixpkgs--coq-buffer-count 0)
        (make-variable-buffer-local 'nixpkgs--is-nixpkgs-coq-buffer)
        (defun nixpkgs--coq-inherit (buf)
          (inherit-local-inherit-child buf)
          (with-current-buffer buf
            (setq nixpkgs--coq-buffer-count (1+ nixpkgs--coq-buffer-count))
            (add-hook 'kill-buffer-hook 'nixpkgs--decrement-coq-buffer-count nil t))
          buf)
        ; When generating a scomint buffer, do inherit-local inheritance and make it a nixpkgs-coq buffer
        (defun nixpkgs--around-scomint-make (orig &rest r)
          (if nixpkgs--is-nixpkgs-coq-buffer
              (progn
                (advice-add 'get-buffer-create :filter-return #'nixpkgs--coq-inherit)
                (apply orig r)
                (advice-remove 'get-buffer-create #'nixpkgs--coq-inherit))
            (apply orig r)))
        (advice-add 'scomint-make :around #'nixpkgs--around-scomint-make)
        ; When we have no more coq buffers, tear down the buffer handling
        (defun nixpkgs--decrement-coq-buffer-count ()
          (setq nixpkgs--coq-buffer-count (1- nixpkgs--coq-buffer-count))
          (when (eq nixpkgs--coq-buffer-count 0)
            (advice-remove 'scomint-make #'nixpkgs--around-scomint-make)
            (fmakunbound 'nixpkgs--around-scomint-make)
            (fmakunbound 'nixpkgs--coq-inherit)
            (fmakunbound 'nixpkgs--decrement-coq-buffer-count))))
      (setq nixpkgs--coq-buffer-count (1+ nixpkgs--coq-buffer-count))
      (add-hook 'kill-buffer-hook 'nixpkgs--decrement-coq-buffer-count nil t)
      (setq nixpkgs--is-nixpkgs-coq-buffer t)
      (inherit-local 'nixpkgs--is-nixpkgs-coq-buffer)
    '';
  };

  src = fetchFromGitHub {
    owner = "coq";
    repo = "coq";
    rev = "V${version}";
    inherit sha256;
  };

  nativeBuildInputs = [ pkgconfig ];
  buildInputs = [ ncurses ocamlPackages.ocaml ocamlPackages.findlib ]
  ++ stdenv.lib.optional (!versionAtLeast "8.10") ocamlPackages.camlp5
  ++ [ ocamlPackages.num ]
  ++ stdenv.lib.optionals buildIde
    (if versionAtLeast "8.10"
     then [ ocamlPackages.lablgtk3-sourceview3 glib gnome3.defaultIconTheme wrapGAppsHook ]
     ++ stdenv.lib.optional stdenv.isDarwin darwin.apple_sdk.frameworks.Cocoa
     else [ ocamlPackages.lablgtk ]);

  postPatch = ''
    UNAME=$(type -tp uname)
    RM=$(type -tp rm)
    substituteInPlace configure --replace "/bin/uname" "$UNAME"
    substituteInPlace tools/beautify-archive --replace "/bin/rm" "$RM"
    substituteInPlace configure.ml --replace '"md5 -q"' '"md5sum"'
    ${csdpPatch}
  '';

  setupHook = writeText "setupHook.sh" ''
    addCoqPath () {
      if test -d "''$1/lib/coq/${coq-version}/user-contrib"; then
        export COQPATH="''${COQPATH-}''${COQPATH:+:}''$1/lib/coq/${coq-version}/user-contrib/"
      fi
    }

    addEnvHooks "$targetOffset" addCoqPath
  '';

  preConfigure = if versionAtLeast "8.10" then ''
    patchShebangs dev/tools/
  '' else ''
    configureFlagsArray=(
      ${ideFlags}
    )
  '';

  prefixKey = "-prefix ";

  buildFlags = [ "revision" "coq" "coqide" "bin/votour" ];

  createFindlibDestdir = true;

  postInstall = ''
    cp bin/votour $out/bin/
    ln -s $out/lib/coq $OCAMLFIND_DESTDIR/coq
  '';

  meta = with stdenv.lib; {
    description = "Coq proof assistant";
    longDescription = ''
      Coq is a formal proof management system.  It provides a formal language
      to write mathematical definitions, executable algorithms and theorems
      together with an environment for semi-interactive development of
      machine-checked proofs.
    '';
    homepage = "http://coq.inria.fr";
    license = licenses.lgpl21;
    branch = coq-version;
    maintainers = with maintainers; [ roconnor thoughtpolice vbgl Zimmi48 ];
    platforms = platforms.unix;
  };
}; in self
generated by cgit v1.2.3 (git 2.25.1) at 2024-08-28 11:08:26 +0000